Universe Polymorphism checking inside opaque terms? (Difference between [Qed.] vs [Opaque]) about coq HOT 7 OPEN

Le 26 juin 2013 à 21:15, Jason Gross [email protected] 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

from coq.

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.

from coq.

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?

from coq.

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

from coq.

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 [email protected] 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.

from coq.

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.

from coq.

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.

from coq.