Universe Polymorphism checking inside opaque terms? (Difference between [Qed.] vs [Opaque])

[JasonGross]

I have some code in a file Functor.v, that when I change two lemmas from Lemma foo : fooT. ... Qed. to Lemma foo : fooT. ... Defined. Global Opaque foo., the time to compile another file shoots up from around 4 minutes to around 90 minutes (I think; I haven't yet fully tracked down the issue, but I'm somewhat confident this is the issue).

With Qeds, the times are:

jgross@cagnode17:~/catdb$ time coqc -q -I . -dont-load-proofs LaxCommaCategory

real    3m47.426s
user    3m45.970s
sys     0m1.300s
jgross@cagnode17:~/catdb$ time coqc -q -I . LaxCommaCategory

real    4m3.526s
user    4m1.895s
sys     0m1.300s

With Defined + Opaque, the time is

real    119m57.947s
user    118m8.419s
sys     0m2.748s

Is universe polymorphism checked differently for Qeded lemmas vs opaque lemmas?

[mattam82]

Le 26 juin 2013 à 21:15, Jason Gross notifications@github.com a écrit :

I have some code in a file Functor.v, that when I change two lemmas from Lemma foo : fooT. ... Qed. to Lemma foo : fooT. ... Defined. Global Opaque foo., the time to compile another file shoots up from around 4 minutes to around 90 minutes (I think; I haven't yet fully tracked down the issue, but I'm somewhat confident this is the issue).

That's quite possible. As others have mentioned on coq-club, the kernel conversion does
not respect opacity information and might hence unfold large proof terms while the unification
algorithm doesn't. Due to the backtracking semantics of unification, if somewhere a unification
failed on a first order unification f t = f u where f is opaque, but succeeded globally, the
kernel conversion will likely take the same path, fail on first order unification as well
but additionally try unifying the expansions of [f], resulting in disastrous performance.
Honoring the opaque flag would endanger subject reduction though. We could reorder conversions
to try expansion at very last resort but that might raise other problems…
Btw, for your performance problems, I'd be curious if you tried branch projbundle of
https://www.pps.univ-paris-diderot.fr/~sozeau/repos/CoqUnivs which contains a version of
Coq deactivating universes but using an optimized representation of record projections.

-- Matthieu

[JasonGross]

I have not tried that branch. I just tried to compile it, and got

$ ./configure -debug -prefix "$(readlink -f ~/.local64)"
...
$ make -j16 -k
...
$ make -j16 -k
make --warn-undefined-variable --no-builtin-rules -f Makefile.build "world"
make[1]: Entering directory `/afs/csail.mit.edu/u/j/jgross/CoqUnivs'
OCAMLDEP  ide/coqide_main_opt.ml
make[1]: Leaving directory `/afs/csail.mit.edu/u/j/jgross/CoqUnivs'
make[1]: Entering directory `/afs/csail.mit.edu/u/j/jgross/CoqUnivs'
CHECK revision
COQC      theories/Numbers/Integer/BigZ/BigZ.v
make[1]: *** [theories/Numbers/Integer/BigZ/BigZ.vo] Segmentation fault
make[1]: *** [theories/Numbers/Integer/BigZ/BigZ.vo] Deleting file `theories/Numbers/Integer/BigZ/BigZ.glob'
make[1]: Target `world' not remade because of errors.
make[1]: Leaving directory `/afs/csail.mit.edu/u/j/jgross/CoqUnivs'
make: *** [world] Error 2
make: Target `NOARG' not remade because of errors.

I will now try it without the -debug flag.

[JasonGross]

I have tried removing the arguments to ./configure; I still get a segfault. Is is possible that my version of ocaml 4.00.1 is too new or something?

[JasonGross]

Oh, oops, that was the master branch. Trying the projbundle branch now.

[mattam82]

Hi Jason,

I think it's the native compiler's fault. Try ./configure with -no-native-compiler.
-- Matthieu

Le 27 juin 2013 à 21:45, Jason Gross notifications@github.com a écrit :

I have not tried that branch. I just tried to compile it, and got

$ ./configure -debug -prefix "$(readlink -f ~/.local64)"
...
$ make -j16 -k
...
$ make -j16 -k
make --warn-undefined-variable --no-builtin-rules -f Makefile.build "world"
make[1]: Entering directory /afs/csail.mit.edu/u/j/jgross/CoqUnivs' OCAMLDEP ide/coqide_main_opt.ml make[1]: Leaving directory/afs/csail.mit.edu/u/j/jgross/CoqUnivs'
make[1]: Entering directory /afs/csail.mit.edu/u/j/jgross/CoqUnivs' CHECK revision COQC theories/Numbers/Integer/BigZ/BigZ.v make[1]: *** [theories/Numbers/Integer/BigZ/BigZ.vo] Segmentation fault make[1]: *** [theories/Numbers/Integer/BigZ/BigZ.vo] Deleting filetheories/Numbers/Integer/BigZ/BigZ.glob'
make[1]: Target world' not remade because of errors. make[1]: Leaving directory/afs/csail.mit.edu/u/j/jgross/CoqUnivs'
make: *** [world] Error 2
make: Target `NOARG' not remade because of errors.
I will now try it without the -debug flag.

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

[JasonGross]

I was able to compile the projbundle branch and attempted to test it. It failed very early, on something equivalent to

Record Foo :=
  {
    foo := 1;
    bar : foo = foo
  }.

with Anomaly: lookup_projection: constant is not a projection. Please report.

[JasonGross]

By the way, I've tried comparing the performance of Coq 8.4 vs HoTT/coq on a small change from Qed to Defined + Opaque. The diff (to be applied to https://bitbucket.org/JasonGross/catdb/commits/4eb6407c6ca3200bebefaa3a1834d05c49b01846), along with a full list of the performance changes, is at https://gist.github.com/JasonGross/5894311. Interestingly, in Coq 8.4, the Defined + Opaque version is about 1 minute (about 7%) slower, picked up entirely in AdjointPointwise.v. In HoTT/coq, the Defined + Opaque version is about 234 minutes (about 220%) slower; 232 of these minutes are picked up in SpecializedLaxCommaCategory.v (largely, I believe, on two failed applys), another minute in AdjointPointwise.v, and the remaining minute scattered across the remaining files.