total2 as record, use of "primitive projections" ? about unimath HOT 29 CLOSED

Here is from an email I wrote in Oct. 2014 when I changed from "record” to ‘Inductive” and removed “primitive projections”:

Just a comment - the whole of UniMath (including RezkCompletion) compiles on my laptop
in about 5min30sec with primitive projections and for about 6min30sec without.

I did it then with the trunk. We should check how it is now with 8.5 before deciding anything.

On Jun 29, 2015, at 12:18 PM, Benedikt Ahrens [email protected] wrote:

As far as I recall, total2 was, at some point, defined as a record type. At the moment, it is defined as an inductive type. (The comments in uuu.v still say that a record type is used.)
What was the reason for changing from record to an ordinary inductive?

If we switched back to total2 being defined as a record type, we could use the "Set Primitive Projections" option which, as @JasonGross https://github.com/JasonGross told me, would provide significant speedup of compilation (at least it did for HoTT/HoTT).
It would also provide eta for dependent pairs, which might or might not be something we want.

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

from unimath.

On 06/29/2015 02:35 PM, Vladimir Voevodsky wrote:

Here is from an email I wrote in Oct. 2014 when I changed from
"record” to ‘Inductive” and removed “primitive projections”:

Just a comment - the whole of UniMath (including RezkCompletion)
compiles on my laptop in about 5min30sec with primitive projections
and for about 6min30sec without.

I did it then with the trunk. We should check how it is now with 8.5
before deciding anything.

It is great to have these measures, thanks. It looks like the benefit
would be small, then, judging from those numbers.

The context of my question is the following: in a development on top of
UniMath [1], we are hitting a point where Qed (or Defined) takes very
long: we have measured 34 minutes for one of them, before starting to
refactor the code significantly. Now the longest Qed takes 11 minutes.

I am thus looking for ways to make UniMath and [1] faster - the
primitive projections are one thing I should look at, is what Jason
Gross said.
There are a few other things I should test, including Opacifying lemmas
temporarily.

Testing primitive projections will need a few changes to UniMath - at
least compilation fails at some point in uu0a for the first time.

Maybe what I would like to suggest is not having primitive projections
in the master branch, but in another branch for testing purposes, with
at least a significant part of UniMath compiling there.

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

from unimath.

What about turning off sharing? Would that speed up your substitution
project?

from unimath.

I tried total2 as a record with primitive projections on, and the failure
point in uu0.v might be
a bug, since the error message includes a new variable, q0, and no new
context for it that tells
what it is.

from unimath.

On 06/29/2015 04:25 PM, Daniel R. Grayson wrote:

I tried total2 as a record with primitive projections on, and the failure
point in uu0.v might be
a bug, since the error message includes a new variable, q0, and no new
context for it that tells
what it is.

Interesting - time to start Jason's bug minimizer!

from unimath.

On 06/29/2015 03:54 PM, Daniel R. Grayson wrote:

What about turning off sharing? Would that speed up your substitution
project?

Thanks for the suggestion. I cannot test right now, being on a
conference, but I'll report back as soon as I have any results.

from unimath.

I'm trying to isolate the uu0a problem, but Jason's bug finder stops after
a certain point,
and it's hard to debug, since it doesn't retain the temporary file it ran
through coq, nor
does it display the command line for running it.

The complete status of what I'm doing is visible on my branch at
https://github.com/DanGrayson/UniMath/tree/primitive-projections ,
where I have a makefile target that will run the bug finder, as a
submodule. Maybe submodules have to be update manually to bring it
in ...

CC-ing Jason.

On Mon, Jun 29, 2015 at 10:50 AM Benedikt Ahrens [email protected]
wrote:

On 06/29/2015 03:54 PM, Daniel R. Grayson wrote:

What about turning off sharing? Would that speed up your substitution
project?

Thanks for the suggestion. I cannot test right now, being on a
conference, but I'll report back as soon as I have any results.

—
Reply to this email directly or view it on GitHub
https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_UniMath_UniMath_issues_111-23issuecomment-2D116713410&d=AwMCaQ&c=8hUWFZcy2Z-Za5rBPlktOQ&r=PAZ_jTPLrSb1btCfAu4RkycWe57N0sGyzbjgeOn2wN0&m=8XgIwPCVZVOiqZRLvjzPkGlRr55GzUSoJ0TpwWtFdC0&s=tP_zXdZoeSfa1FQFNmbyXWGRPQUDxSlpjIx9bBu4Y3w&e=
.

from unimath.

On Jun 29, 2015, at 3:41 PM, Benedikt Ahrens [email protected] wrote:

The context of my question is the following: in a development on top of
UniMath [1], we are hitting a point where Qed (or Defined) takes very
long: we have measured 34 minutes for one of them, before starting to
refactor the code significantly. Now the longest Qed takes 11 minutes.

I would say that this means something is wrong in the approach. Probably more layers of abstraction (in the mathematical sense) are needed so that the proofs do not need to expand too many definitions (in proof assistant terms).

This whole thing looks a bit strange to me since it is based on http://www.irit.fr/%7ERalph.Matthes/papers/MatthesUustalu-final.pdf http://www.irit.fr/~Ralph.Matthes/papers/MatthesUustalu-final.pdf and the later approach by Andre and Marco seem to be conceptually much better.

In terms of locating where things start going wrong I would suggest that any proof that requires more than 30sec at the Qed is an indication that some bad choices have been made upstream and need to be corrected.

Vladimir.

from unimath.

since it doesn't retain the temporary file it ran
through coq, nor
does it display the command line for running it.

Try passing -vv or -vvv for more verbose output. (If you pass -vvv or -vvvv, I think it might also print the full contents of each file it tries to run through coq.) If you update to the latest version of the bug-minimizer, it should print the command lines it uses. If you also pass a third argument (find-bug.py in_file.v out_file.v temp_file.v), and a particular coq run fails, it should save the attempt in that temporary file.

from unimath.

On 06/29/2015 07:42 PM, Vladimir Voevodsky wrote:

I would say that this means something is wrong in the approach.
Probably more layers of abstraction (in the mathematical sense) are
needed so that the proofs do not need to expand too many definitions
(in proof assistant terms).

I agree. We are looking into that, too, in parallel to improvements we
could do on the technical side.

This whole thing looks a bit strange to me since it is based on
http://www.irit.fr/%7ERalph.Matthes/papers/MatthesUustalu-final.pdf
http://www.irit.fr/~Ralph.Matthes/papers/MatthesUustalu-final.pdf
and the later approach by Andre and Marco seem to be conceptually
much better.

The notion of signature in Matthes & Uustalu's paper is pretty similar
to the one André and Marco are giving in [1].

The notion of model of a signature is different, and I agree that M&U's
notion is unsatisfactory in some ways.
On the other hand, I have implemented monads and modules and all that
stuff in my PhD thesis already (based on E-categories, i.e., categories
with hom-setoids) [2], and it is fun to do something else for a change.

[1] http://arxiv.org/abs/1202.3499
[2] https://github.com/benediktahrens/monads

In terms of locating where things start going wrong I would suggest
that any proof that requires more than 30sec at the Qed is an
indication that some bad choices have been made upstream and need to
be corrected.

Yes, that sounds very reasonable.

from unimath.

On Mon, Jun 29, 2015 at 3:25 PM Jason Gross [email protected]
wrote:

since it doesn't retain the temporary file it ran
through coq, nor
does it display the command line for running it.

Try passing -vv or -vvv for more verbose output. (If you pass -vvv or
-vvvv, I think it might also print the full contents of each file it
tries to run through coq.)

Thanks. Hmm, -vv is already annoyingly verbose, and it doesn't
seem to display the file. What about just keeping temporary files that are
unsuccessful, and always displaying the command line?

If you update to the latest version of the bug-minimizer, it should print
the command lines it uses.

We are up to date, at commit acbb5bf2f1ee3c050973ead4531be55efeec26cb.
Here's the part of the output with no command line echoed:

Done. Splitting to definitions...

Non-fatal error: Failed to split file to definitions and preserve the
error.
The new error was:
File "/var/folders/46/9b86vqxj4hjcngvy7kd7sb140000gn/T/tmpKKShIU.v", line
4, characters 7-13:
Syntax error: '.' expected after [vernac:gallina_ext](in [vernac_aux]).

Split not saved.
I will not be able to proceed.

If you also pass a third argument (find-bug.py in_file.v out_file.v
temp_file.v), and a particular coq run fails, it should save the attempt
in that temporary file.

—
Reply to this email directly or view it on GitHub
https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_UniMath_UniMath_issues_111-23issuecomment-2D116805684&d=AwMCaQ&c=8hUWFZcy2Z-Za5rBPlktOQ&r=PAZ_jTPLrSb1btCfAu4RkycWe57N0sGyzbjgeOn2wN0&m=8ueLLXREpeSd5i8eg6epqXRiH8kpQb9e3TGHVkh77q0&s=aDkKRxNTKfrPXNeKlHG2YbkSAujPabw4RN76SlorC9M&e=
.

from unimath.

Hmm, I guess the "problem" is not just the error message, but also that there even is an error.

from unimath.

I submitted a bug report here: https://coq.inria.fr/bugs/show_bug.cgi?id=4273

(After a month and a half the bug report has attracted no attention or response. Perhaps I'll have a go at debugging it.)

from unimath.

This is a very interesting place to discover a problem. The constructions of this theorem (onefiber’ as opposed to onefiber) were invented to avoid the use of a complex match (in the proof of onefiber) and to do everything with induction (eliminators) instead. As such it is an important place in uu0 and we should certainly investigate further.

from unimath.

Matthieu fixed that bug last week, and since then I've reported two bugs:

https://coq.inria.fr/bugs/show_bug.cgi?id=4417
https://coq.inria.fr/bugs/show_bug.cgi?id=4418

The first one is in "apply" -- a work-around suggested by Matthieu is to use "refine" instead. That helps.

(The first one has since been fixed.)

The second bug report is more puzzling. Also it shows the execution time of Coq increasing by a multiple of 5 when primitive projections are on, so we may never want to use them.

from unimath.

Matthieu responded to the second bug here:

https://coq.inria.fr/bugs/show_bug.cgi?id=4418#c2

The interesting thing is that he gets dramatic speed-ups simply by replacing "apply"
by "refine".

from unimath.

I took another stab at switching our code to using primitive projections (which would
provide eta for pairs) and ran into a bug on the trunk of Coq which I've reported here:

https://coq.inria.fr/bugs/show_bug.cgi?id=4876

Thanks to @JasonGross for his bug isolator!

Latest changes are here: https://github.com/DanGrayson/UniMath/tree/primitive-projections

from unimath.

I seem to recall Set Keyed Unification fixing a few issues with rewrite and Set Primitive Projections; does this setting (together with Declare Equivalent Keys when you need two head constants to be considered the same) help?

from unimath.

No, Declare Equivalent Keys doesn't help, and I don't know which two head
constants you have in mind for me.

from unimath.

Try Set Keyed Unification. Declare Equivalent Keys unel natmult.?

from unimath.

Nope, that didn't help.

from unimath.

Oh! You were trying to rewrite on the LHS, not the RHS. Try Set Keyed Unification. Declare Equivalent Keys natmult op. Declare Equivalent Keys natmult unel.? I'm not quite sure if this'll work, though.
@mattam82 might need to provide the right incantation to get natmult (S 0) x to unfold into (op (pr1 X) x (natmult 0 x)) and then get natmult 0 x to unfold into unel x so that it matches with op (pr1 ?M194) ?M195 (unel ?M194).

from unimath.

Meanwhile, I've submitted #393

from unimath.

No, that didn't work either.

I'm content to wait for the bug fix.

from unimath.

The bug at https://coq.inria.fr/bugs/show_bug.cgi?id=4876 is fixed and the fix will appear in the next patch level for v8.5 of Coq. The fix is part of commit ba00867d515624aee734d998bfbe3880f559d907.

from unimath.

I tried again and got stuck with a Coq bug, reported here: https://coq.inria.fr/bugs/show_bug.cgi?id=5063 -- but it may not be a bug.

I'm currently working with primitive projections on this branch: https://github.com/DanGrayson/UniMath/tree/primitive-projections-2

These changes (part of DanGrayson@cd51d63) seemed to work around the bug just reported, but they don't work with primitive projections off, so it's good to get a bug fix:

diff --git a/UniMath/Foundations/Algebra/Archimedean.v b/UniMath/Foundations/Algebra/Archimedean.v
index 121e7ee..ba2cebd 100644
--- a/UniMath/Foundations/Algebra/Archimedean.v
+++ b/UniMath/Foundations/Algebra/Archimedean.v
@@ -491,8 +492,8 @@ Proof.
     apply hinhfun.
     intros n.
     exists (pr1 n).
-    abstract (pattern x at 2 ; rewrite <- (riglunax1 X x) ;
-              pattern (0%rig : X) at 2 ; rewrite <- (rigmultx0 X (nattorig (pr1 n))) ;
+    abstract (pattern x ; rewrite <- (riglunax1 X x) ;
+              pattern (0%rig : X) ; rewrite <- (rigmultx0 X (nattorig (pr1 n))) ;
               rewrite nattorig_natmult ;
               exact (pr2 n)).
   - intros x.
@@ -500,7 +501,7 @@ Proof.
     apply hinhfun.
     intros n.
     exists (pr1 n).
-    abstract (pattern (0%rig : X) at 2 ;
+    abstract (pattern (0%rig : X) ;
                rewrite <- (rigmultx0 X (nattorig (pr1 n))), nattorig_natmult ;
                exact (pr2 n)).
 Defined.

from unimath.

I reported another Coq bug here: https://coq.inria.fr/bugs/show_bug.cgi?id=5064 , but it's not a bug. Instead, one has to expect expressions to differ with primitive projections on, because the subexpressions corresponding to parameters of pr1 and pr2 will no longer be present.

from unimath.

I reported another Coq bug here: https://coq.inria.fr/bugs/show_bug.cgi?id=5068

It's now been reported fixed by commit coq/coq@405acea. The fix works, but currently it's just on the v8.6 branch. I've asked them to include it in v8.5.

from unimath.

I reported another coq bug here: https://coq.inria.fr/bugs/show_bug.cgi?id=5105

from unimath.