Switch to Coq 8.5 about unimath HOT 46 CLOSED

I tried that at https://github.com/DanGrayson/UniMath/commits/update-for-coq-trunk-unpatched and coq crashed, and I wasn't able to debug it. But of course, we should return to that.

from unimath.

On 05/11/2015 03:23 AM, Daniel R. Grayson wrote:

I tried that at
https://github.com/DanGrayson/UniMath/commits/update-for-coq-trunk-unpatched
and coq crashed, and I wasn't able to debug it. But of course, we
should return to that.

I have tried to change to vanilla Coq for the git submodule, see branch
for-8.5 of my fork [1].
However, I did not get far:
$ make
Makefile:66: *** target file `clean' has both : and :: entries. Stop.

A related question: In case we can use vanilla Coq 8.5, should we still
carry it around as a submodule?
Maybe it makes sense to modularize the system a bit, by making Coq 8.5 a
dependency rather than part of the installation.

1. People might already have a suitable installation of Coq on their
   machine, and
2. we might get a less complicated Makefile.

[1] https://github.com/benediktahrens/UniMath

from unimath.

I am very much for it. I think it is a major milestone for us to be able to use of-the-shelf Coq.

Vladimir.

On May 11, 2015, at 12:23 AM, Benedikt Ahrens [email protected] wrote:

Is it too early to think about switching to Coq 8.5?
Using the type-in-type flag (and -indices-matter), it should be possible to stick to vanilla Coq.
Maybe we should start a branch to gather some work towards that switch? It might take a while to adapt all the packages.

—
Reply to this email directly or view it on GitHub #92.

from unimath.

@DanGrayson : the tip of the branch you indicate fails even to start comiling:

$ make 
Makefile:28: build/CoqMakefile.make: No such file or directory
making .coq_makefile_input
make: *** No rule to make target `sub/coq/configure.ml', needed by `sub/coq/config/coq_config.ml'.  Stop.

Do you remember when coq crashed in your tests?

I have made a branch "for-8.5-std-makefile" where I only use a simple wrapper script around the standard Coq Makefile.
Having Coq8.5beta2 [1] in my path, the first problem seems to be that a lot of "induction e" have to be replaced by "destruct e" for e being some path.
[1] https://github.com/coq/coq/releases/tag/V8.5beta2

One thing that I couldn't get to work: passing options "indices-matter" and "type-in-type" to coqc via coq_makefile. So for now I have to call make via

make COQC="coqc -indices-matter -type-in-type"

If you know how to do it properly, please let me know.

from unimath.

Another issue was getting the identity type to be in the right universe.
To this end, it suffices to redefine it in uuu.v:
benediktahrens@8016d4c

Now I have a more difficult problem:

$ make
"coqc"  -q  -R "." UniMath -type-in-type -indices-matter  UniMath/Foundations/Generalities/uu0c
File "./UniMath/Foundations/Generalities/uu0c.v", line 841, characters 0-100:
Anomaly: Uncaught exception Term.DestKO. Please report.
make: *** [UniMath/Foundations/Generalities/uu0c.vo] Error 1

from unimath.

It seems that "Uncaught exception Term.DestKO. Please report." is just Coq's way of saying that it cannot infer some implicit arguments - at least, indicating an implicit argument fixed this problem in the first occurrence in uu0c.v.
However, the same problem occurs later in places with more obscure statements, where it is not clear to me at first sight what the statement is supposed to say.
Feel free to have a go at it in my branch "for-8.5-std-makefile".
EDIT: I moved the Makefile one level further down, into UniMath/UniMath, to work around an obscure problem with Require commands.

from unimath.

The anomaly is a bug in Coq. Do you want to turn it into a small test case and report it with my coq-bug-minimizer?

from unimath.

On 05/11/2015 04:43 PM, Jason Gross wrote:

The anomaly is a bug in Coq. Do you want to turn it into a small
test case and report it with my coq-bug-minimizer?

Interesting suggestion - I'll try.

I have two questions:
a) where should I call the program from - the same directory I call
'make' from?
b) where should I drop the python files?

Thanks for your help.
b

from unimath.

Oh, and
c) how do I pass the extra arguments "-indices-matter" and "-type-in-type" to coqc ?

from unimath.

a) It works best if you call it from the directory that UniMath is bound to
b) anywhere, as long as the python files are in the same directory as each other
c) You want an invocation like this:

python /path/to/coq-tools/find-bug.py Foundations/Generalities/uu0c.v bug_uu0c_anomaly_dest_ko_01.v -R . UniMath -arg " -indices-matter" -arg " -type-in-type"

(note the spaces before -indices-matter and -type-in-type; these work around an infelicity in python's argparse module)
(you can optionally pass --minimize-before-inlining if uu0c has lots of dependencies that this lemma won't need, or if its dependencies are very long files, and you want to strip out the stuff in uu0c before including its dependencies.)

An alternative to passing these these things on the command-line is to include

(* -*- coq-prog-args: ("-emacs" "-indices-matter" "-type-in-type") -*- *)

at the top of the .v file.

from unimath.

Thanks for your help - bug is filed at https://coq.inria.fr/bugs/show_bug.cgi?id=4234.
The tool did a great job - perfect, actually. I chose this particular problem, because it seemed to be well minimizable, but I am still surprised at how well it worked.

from unimath.

The bug is now fixed in commit a49cd60c67aca452500c82aad61327823f9abe31 of Coq.
The next problem is Coq dying with "Out of memory" during the compilation of algebra1b:
"coqc" -q -R "." UniMath -type-in-type -indices-matter Foundations/hlevel2/algebra1b
Fatal error: out of memory.
make: *** [Foundations/hlevel2/algebra1b.vo] Error 2
More precisely, this happens in the "Defined." of "ispartlbinopabmonoidfracrel", line 497 of algebra1b.

If I remember correctly, a fix for similar such issues was to make parts of the terms opaque within the proof, right?
Are there any tricks to debug this kind of problem, or is it trial and error?

from unimath.

Try Set Kernel Term Sharing or Unset Kernel Term Sharing. You can stick this, with a Global in front of it, in uuu.v or whatever is imported everywhere to get the same effect as the -no-sharing option from your patched version of Coq.

from unimath.

That was a quick bug fix!

On Tue, May 12, 2015 at 8:12 AM Benedikt Ahrens [email protected]
wrote:

The bug is now fixed in commit a49cd60c67aca452500c82aad61327823f9abe31 of
Coq.
The next problem is Coq dying with "Out of memory" during the compilation
of algebra1b:
"coqc" -q -R "." UniMath -type-in-type -indices-matter
Foundations/hlevel2/algebra1b
Fatal error: out of memory.
make: *** [Foundations/hlevel2/algebra1b.vo] Error 2
More precisely, this happens in the "Defined." of
"ispartlbinopabmonoidfracrel", line 497 of algebra1b.

If I remember correctly, a fix for similar such issues was to make parts
of the terms opaque within the proof, right?
Are there any tricks to debug this kind of problem, or is it trial and
error?

—
Reply to this email directly or view it on GitHub
#92 (comment).

from unimath.

On 05/12/2015 03:31 PM, Daniel R. Grayson wrote:

That was a quick bug fix!

Well, Jason told them exactly how to fix it!

from unimath.

In my branch for-8.5-std-makefile there is now a version of UniMath which compiles with Coq 8.5 (thanks to Jason and the Coq team), more precisely with commit a49cd60c67aca452500c82aad61327823f9abe31 (which is in branch 8.5-dev). The code in the branch is not very clean, but it is instructive to have a look at the modifications that need to be made in order to switch to standard Coq 8.5 - see [1] for a diff with current UniMath master.

In order to switch to standard Coq, I suggest not to install Coq through our Makefile, but to leave it up to the user to install Coq (we can still give precise instructions of how to do so, but its installation should really not be our concern).

[1] master...benediktahrens:for-8.5-std-makefile

from unimath.

Great, thanks!!

On Tue, May 12, 2015 at 1:34 PM Benedikt Ahrens [email protected]
wrote:

In my branch for-8.5-std-makefile there is now a version of UniMath which
compiles with Coq 8.5 (thanks to Jason and the Coq team), more precisely
with commit a49cd60c67aca452500c82aad61327823f9abe31 (which is in branch
8.5-dev). The code in the branch is not very clean, but it is instructive
to have a look at the modifications that need to be made in order to switch
to standard Coq 8.5 - see [1] for a diff with current UniMath master.

In order to switch to standard Coq, I suggest not to install Coq through
our Makefile, but to leave it up to the user to install Coq (we can still
give precise instructions of how to do so, but its installation should
really not be our concern).

[1] master...benediktahrens:for-8.5-std-makefile
master...benediktahrens:for-8.5-std-makefile

—
Reply to this email directly or view it on GitHub
#92 (comment).

from unimath.

Probably we have to keep compiling in sub/coq as before until the current version of coq, with
the bug fix, is distributed in one of their standard releases.

What's the point of moving the Makefile? Why introduce UniMath/Make? (it duplicates the
file names in UniMath/*/.package/files.)

from unimath.

On 05/12/2015 09:19 PM, Daniel R. Grayson wrote:

Probably we have to keep compiling in sub/coq as before until the current version of coq, with
the bug fix, is distributed in one of their standard releases.

Right. Maybe we can wait with the switch until after the release?
It seems a good idea to continuously check that no new bugs are
introduced in Coq, that affect our code, but we can do that outside the
UniMath repository.

What's the point of moving the Makefile? Why introduce UniMath/Make? (it duplicates the
file names in UniMath/*/.package/files.)

Since I was having some trouble with the current Makefile, I switched to
the "standard" way of making a Makefile in Coq, which is via a Make
file. Also, this was the only way I was able to pass the arguments to coqc.

After switching to the standard Make -> Makefile way, I had a weird
error when compiling uu0c, complaining about uu0b being
UniMath.UniMath.Foundations.Generalities.uu0b
instead of
UniMath.Foundations.Generalities.uu0b (or the other way round).
I was not able to figure out the problem - uu0b did not give any trouble
when importing uu0a, and the Require looked the same.

But the problem went away when I moved everything one directory down.

I have not investigated further, since my goal was to test the Coq code.
Of course, someone should have a look at the Require issue, too - if it
is still an issue at all, and not a consequence of incomplete cleaning
or similar of mine.

from unimath.

Re: "It seems a good idea to continuously check that no new bugs are
introduced in Coq, that affect our code, but we can do that outside the
UniMath repository."

Yes, but for me, at least, it would be easier if the procedure for updating and recompiling
coq to the latest version continued to be automated, as it currently is. And
for other people who want to get started now and not to wait, it would be good
not to have to give them instructions about building coq on their machines.

Re: "Since I was having some trouble with the current Makefile, I switched to
the "standard" way of making a Makefile in Coq, which is via a Make
file. Also, this was the only way I was able to pass the arguments to coqc."

Well, the old Makefile also uses that standard way of making a makefile. The name of it
is .coq_makefile_input -- the advantage is that the makefile makes it from the files maintained
by the individual package developers, making things simpler for them. It also allows
arguments to be passed to coqc, or could be made easily to do so. I'd be happy to restore
things so they work, and to take a look at the "UniMath." naming issue, later on.

from unimath.

The current way to pass options to coqc is with the make variable OTHERFLAGS,
and it works.

from unimath.

PS: OTHERFLAGS is one of the variables used in the makefile made by coq_makefile.

from unimath.

coq_makefile has a -arg option; you can do something like coq_makefile -arg -indices-matter ...

from unimath.

On 05/12/2015 09:50 PM, Daniel R. Grayson wrote:

Re: "It seems a good idea to continuously check that no new bugs are
introduced in Coq, that affect our code, but we can do that outside the
UniMath repository."

Yes, but for me, at least, it would be easier if the procedure for updating and recompiling
coq to the latest version continued to be automated, as it currently is. And
for other people who want to get started now and not to wait, it would be good
not to have to give them instructions about building coq on their machines.

Re: "Since I was having some trouble with the current Makefile, I switched to
the "standard" way of making a Makefile in Coq, which is via a Make
file. Also, this was the only way I was able to pass the arguments to coqc."

Well, the old Makefile also uses that standard way of making a makefile. The name of it
is .coq_makefile_input -- the advantage is that the makefile makes it from the files maintained
by the individual package developers, making things simpler for them. It also allows
arguments to be passed to coqc, or could be made easily to do so. I'd be happy to restore
things so they work, and to take a look at the "UniMath." naming issue, later on.

When I started converting to Coq 8.5, I had some weirdness with the
current Makefile - I can't remember, but it seemed to look like the
issue Anders mentioned.
Since I did not want to be bothered by that, I switched to something I
know and understand.

Branch for-8.5-std-makefile is not about suggesting a change to the
Makefile. But the Makefile there was the only one that worked for me.
I am also not suggesting to merge that branch.

If you can provide a clean way of doing things, that would be awesome -
maybe starting with a fresh branch of master. It should be easy enough
to reproduce the necessary changes to UniMath by looking at the diff at
master...benediktahrens:for-8.5-std-makefile
.

from unimath.

Also, note that some earlier commits of https://github.com/benediktahrens/UniMath/commits/for-8.5-std-makefile are probably not needed, since they were to work around bug https://coq.inria.fr/bugs/show_bug.cgi?id=4234 .

from unimath.

Okay, I'll take a stab at it, thanks for the suggestion.

On Tue, May 12, 2015 at 3:31 PM Benedikt Ahrens [email protected]
wrote:

Also, note that some earlier commits of
https://github.com/benediktahrens/UniMath/commits/for-8.5-std-makefile
are probably not needed, since they were to work around bug
https://coq.inria.fr/bugs/show_bug.cgi?id=4234 .

—
Reply to this email directly or view it on GitHub
#92 (comment).

from unimath.

Great! Vladimir.

On May 12, 2015, at 8:34 PM, Benedikt Ahrens <[email protected] mailto:[email protected]> wrote:

In my branch for-8.5-std-makefile there is now a version of UniMath which compiles with Coq 8.5 (thanks to Jason and the Coq team), more precisely with commit a49cd60c67aca452500c82aad61327823f9abe31 (which is in branch 8.5-dev). The code in the branch is not very clean, but it is instructive to have a look at the modifications that need to be made in order to switch to standard Coq 8.5 - see [1] for a diff with current UniMath master.

In order to switch to standard Coq, I suggest not to install Coq through our Makefile, but to leave it up to the user to install Coq (we can still give precise instructions of how to do so, but its installation should really not be our concern).

[1] master...benediktahrens:for-8.5-std-makefile master...benediktahrens:for-8.5-std-makefile
—
Reply to this email directly or view it on GitHub #92 (comment).

from unimath.

I'm starting to work on that in https://github.com/DanGrayson/UniMath/tree/for-coq-trunk-unpatched , following your changes one by one. I've started by making my old makefile compile the latest coq, with the fix for the bug you reported.

I think those earlier commits you mentioned might have worked around a different bug, because
now I get Anomaly: Uncaught exception Term.DestKO before applying any of your patches to the proofs. I think I'll isolate and report the bug, as you did -- it will save trouble in the long run.

from unimath.

Try bumping the coq version again to f86b7d3 or newer; there've been two fixes for DestKO. If that doesn't fix it, if you run coqc with -debug, the last three lines in the trace would be useful. (A minimized test-case will also be useful.) Also, I think you want to use the v8.5 branch, not the trunk branch, of Coq. (The fixes are both on the v8.5 branch, and haven't been merged back into trunk, yet.)

from unimath.

Oh, thanks!

By the way, in trying to run your bug minimizer, I get this mystical problem, which I hope you can shed some light on:

einsteinium-dan-macbook-pro$ rm -f bug.v ; ../Gross-tools/find-bug.py --coqtop sub/coq/bin/coqtop --arg " -indices-matter" --arg " -type-in-type" -R "UniMath" UniMath UniMath/Foundations/Generalities/uu0c.v bug.v

First, I will attempt to inline all of the inputs in UniMath/Foundations/Generalities/uu0c.v, and store the result in bug.v...
getting UniMath/UniMath/Foundations/Generalities/uu0c.v
remaining imports:
['UniMath.UniMath.Foundations.Generalities.uu0c']
Stripping trailing ends

Now, I will attempt to coq the file, and find the error...

Coqing the file (bug.v)...
The timeout has been set to: 2

This file produces the following output when Coq'ed:
coqc: -indices-matter: no such file or directory

Does this output display the correct error? [(y)es/(n)o]   C-c C-cTraceback (most recent call last):
  File "../Gross-tools/find-bug.py", line 1218, in <module>
    env['error_reg_string'] = get_error_reg_string(output_file_name, **env)
  File "../Gross-tools/find-bug.py", line 223, in get_error_reg_string
    result = raw_input('Does this output display the correct error? [(y)es/(n)o] ').lower().strip()
KeyboardInterrupt
einsteinium-dan-macbook-pro$ sub/coq/bin/coqtop -indices-matter
Welcome to Coq trunk (May 2015)

Coq < 

from unimath.

You need to also pass --coqc sub/coq/bin/coqc; Coq gives that mystical error message when it doesn't recognize an option you give it, and tries to interpret it as a file.

from unimath.

Also, the bug minimizer currently seems to not to support -R some_directory UniMath, only -R . UniMath (you'll need to cd to inside UniMath); I'll see if I can fix this.

from unimath.

Could you also arrange for the command line it's running to be printed? I could have debugged the mystical problem myself if I had seen it.

from unimath.

Could you also arrange for the command line it's running to be printed? I could have debugged the mystical problem myself if I had seen it.

Done.

from unimath.

Thanks!

from unimath.

Benedikt, I'm omitting changes of yours like this:

 Definition pathsinv0l {X : UU} {a b : X} (e : a = b) : !e @ e = idpath _.
 Proof.
-  intros. induction e. apply idpath.
+  intros. destruct e. apply idpath.
 Defined.

 Definition pathsinv0r {X : UU} {a b : X} (e : a = b) : e @ !e = idpath _.
 Proof.
-  intros. induction e. apply idpath.
+  intros. destruct e. apply idpath.
 Defined. 

 Definition pathsinv0inv0 {X : UU} {x x' : X} (e : x = x') : !(!e) = e.
 Proof.
-  intros. induction e. apply idpath.
+  intros. destruct e. apply idpath.
 Defined.

because Vladimir wants to use just paths_rect. Is that okay?

from unimath.

On 05/13/2015 11:37 PM, Daniel R. Grayson wrote:

Benedikt, I'm omitting changes of yours like this:

 Definition pathsinv0l {X : UU} {a b : X} (e : a = b) : !e @ e = idpath _.
 Proof.
-  intros. induction e. apply idpath.
+  intros. destruct e. apply idpath.
 Defined.

because Vladimir wants to use just paths_rect. Is that okay?

I changed those because "induction" did not work - in general I did not
change stuff that worked.
Maybe "induction " did not work for me because I had not set the
"-indices-matters" flag?
But that would be weird, because that flag is part of my emacs dir-local
file, so it should be automatic.

Anyway, if it works as it is, that is, if those changes are not needed,
then they should be omitted.

Thanks for working on this.

from unimath.

It's all working now. Here are some timing logs; notice that compiling in
parallel does give some speed up. I'll try telling travis to compile in parallel.

==> TIMING-LOG-patched-coq <==
0.83user 0.15system 0:00.99elapsed 99%CPU (0avgtext+0avgdata 1434828800maxresident)k
0inputs+7outputs (0major+88249minor)pagefaults 0swaps
242.21user 7.84system 4:10.48elapsed 99%CPU (0avgtext+0avgdata 2163474432maxresident)k
0inputs+84outputs (2major+4335278minor)pagefaults 0swaps

==> TIMING-LOG-standard-coq <==
0.73user 0.13system 0:00.87elapsed 99%CPU (0avgtext+0avgdata 1468448768maxresident)k
0inputs+1outputs (0major+90382minor)pagefaults 0swaps
218.72user 7.62system 4:42.30elapsed 80%CPU (0avgtext+0avgdata 1588346880maxresident)k
0inputs+121outputs (0major+4387137minor)pagefaults 0swaps

==> TIMING-LOG-standard-coq-in-parallel <==
1.47user 0.13system 0:01.61elapsed 99%CPU (0avgtext+0avgdata 1446313984maxresident)k
0inputs+1outputs (0major+89034minor)pagefaults 0swaps
223.62user 8.42system 3:03.47elapsed 126%CPU (0avgtext+0avgdata 1589215232maxresident)k
0inputs+98outputs (0major+4405813minor)pagefaults 0swaps

from unimath.

There's probably no point telling travis to compile in parallel, because it's probably running
in a virtual machine. But I'm telling it to time the compilation steps, so we can tell if something
slows down.

from unimath.

What is the context of this discussion? Why did these changes appeared?

Vladimir.

On May 13, 2015, at 11:37 PM, Daniel R. Grayson [email protected] wrote:

Benedikt, I'm omitting changes of yours like this:

Definition pathsinv0l {X : UU} {a b : X} (e : a = b) : !e @ e = idpath _.
Proof.

• intros. induction e. apply idpath.
• intros. destruct e. apply idpath.
  Defined.

Definition pathsinv0r {X : UU} {a b : X} (e : a = b) : e @ !e = idpath _.
Proof.

• intros. induction e. apply idpath.
• intros. destruct e. apply idpath.
  Defined.

Definition pathsinv0inv0 {X : UU} {x x' : X} (e : x = x') : !(!e) = e.
Proof.

• intros. induction e. apply idpath.
• intros. destruct e. apply idpath.
  Defined.
  because Vladimir wants to use just paths_rect. Is that okay?

—
Reply to this email directly or view it on GitHub #92 (comment).

from unimath.

This is timing for what?
Vladimir.

On May 14, 2015, at 1:15 AM, Daniel R. Grayson [email protected] wrote:

It's all working now. Here are some timing logs; notice that compiling in
parallel does give some speed up. I'll try telling travis to compile in parallel.

==> TIMING-LOG-patched-coq <==
0.83user 0.15system 0:00.99elapsed 99%CPU (0avgtext+0avgdata 1434828800maxresident)k
0inputs+7outputs (0major+88249minor)pagefaults 0swaps
242.21user 7.84system 4:10.48elapsed 99%CPU (0avgtext+0avgdata 2163474432maxresident)k
0inputs+84outputs (2major+4335278minor)pagefaults 0swaps

==> TIMING-LOG-standard-coq <==
0.73user 0.13system 0:00.87elapsed 99%CPU (0avgtext+0avgdata 1468448768maxresident)k
0inputs+1outputs (0major+90382minor)pagefaults 0swaps
218.72user 7.62system 4:42.30elapsed 80%CPU (0avgtext+0avgdata 1588346880maxresident)k
0inputs+121outputs (0major+4387137minor)pagefaults 0swaps

==> TIMING-LOG-standard-coq-in-parallel <==
1.47user 0.13system 0:01.61elapsed 99%CPU (0avgtext+0avgdata 1446313984maxresident)k
0inputs+1outputs (0major+89034minor)pagefaults 0swaps
223.62user 8.42system 3:03.47elapsed 126%CPU (0avgtext+0avgdata 1589215232maxresident)k
0inputs+98outputs (0major+4405813minor)pagefaults 0swaps
—
Reply to this email directly or view it on GitHub #92 (comment).

from unimath.

I had to make these changes in a first attempt to switch to Coq 8.5 (for
a reason that I don't understand).
But now Dan Grayson says that they are not necessary, so those changes
are thrown away.

On 05/14/2015 12:15 PM, Vladimir Voevodsky wrote:

What is the context of this discussion? Why did these changes appeared?

Vladimir.

On May 13, 2015, at 11:37 PM, Daniel R. Grayson [email protected] wrote:

Benedikt, I'm omitting changes of yours like this:

Definition pathsinv0l {X : UU} {a b : X} (e : a = b) : !e @ e = idpath _.
Proof.

• intros. induction e. apply idpath.
• intros. destruct e. apply idpath.
  Defined.

Definition pathsinv0r {X : UU} {a b : X} (e : a = b) : e @ !e = idpath _.
Proof.

• intros. induction e. apply idpath.
• intros. destruct e. apply idpath.
  Defined.

Definition pathsinv0inv0 {X : UU} {x x' : X} (e : x = x') : !(!e) = e.
Proof.

• intros. induction e. apply idpath.
• intros. destruct e. apply idpath.
  Defined.
  because Vladimir wants to use just paths_rect. Is that okay?

—
Reply to this email directly or view it on GitHub #92 (comment).

---

Reply to this email directly or view it on GitHub:
#92 (comment)

from unimath.

That's timing for running Coq on all our proofs, three ways: using our
patched Coq, using standard Coq 8.5, and using 8.5 with make running 4 jobs
at a time.

On Thu, May 14, 2015, 05:41 Vladimir Voevodsky [email protected]
wrote:

This is timing for what?
Vladimir.

On May 14, 2015, at 1:15 AM, Daniel R. Grayson [email protected]
wrote:

It's all working now. Here are some timing logs; notice that compiling
in
parallel does give some speed up. I'll try telling travis to compile in
parallel.

==> TIMING-LOG-patched-coq <==
0.83user 0.15system 0:00.99elapsed 99%CPU (0avgtext+0avgdata
1434828800maxresident)k
0inputs+7outputs (0major+88249minor)pagefaults 0swaps
242.21user 7.84system 4:10.48elapsed 99%CPU (0avgtext+0avgdata
2163474432maxresident)k
0inputs+84outputs (2major+4335278minor)pagefaults 0swaps

==> TIMING-LOG-standard-coq <==
0.73user 0.13system 0:00.87elapsed 99%CPU (0avgtext+0avgdata
1468448768maxresident)k
0inputs+1outputs (0major+90382minor)pagefaults 0swaps
218.72user 7.62system 4:42.30elapsed 80%CPU (0avgtext+0avgdata
1588346880maxresident)k
0inputs+121outputs (0major+4387137minor)pagefaults 0swaps

==> TIMING-LOG-standard-coq-in-parallel <==
1.47user 0.13system 0:01.61elapsed 99%CPU (0avgtext+0avgdata
1446313984maxresident)k
0inputs+1outputs (0major+89034minor)pagefaults 0swaps
223.62user 8.42system 3:03.47elapsed 126%CPU (0avgtext+0avgdata
1589215232maxresident)k
0inputs+98outputs (0major+4405813minor)pagefaults 0swaps
—
Reply to this email directly or view it on GitHub <
https://github.com/UniMath/UniMath/issues/92#issuecomment-101845651>.

—
Reply to this email directly or view it on GitHub
#92 (comment).

from unimath.

Why not write pathsinv0l and the others directly using paths_rect?

Definition pathsinv0l {X : UU} {a b : X} (e : a = b) : !e @ e = idpath _ :=
  paths_rect a (fun b e => ! e @ e = idpath b) (idpath (idpath a)) b e.

This way the definition does not depend on the behavior of any tactics that might change with future releases and you are sure that it is what you expect.

from unimath.

It sounds like a good idea for such fundamental definitions.

On May 15, 2015, at 10:24 AM, mortberg [email protected] wrote:

Why not write pathsinv0l and the others directly using paths_rect?

Definition pathsinv0l {X : UU} {a b : X} (e : a = b) : !e @ e = idpath _ :=
paths_rect a (fun b e => ! e @ e = idpath b) (idpath (idpath a)) b e.

This way the definition does not depend on the behavior of any tactics that might change with future releases and you are sure that it is what you expect.

—
Reply to this email directly or view it on GitHub #92 (comment).

from unimath.

This issue has been resolved, closing.

from unimath.