Forcing normalization in Coq

[JasonGross]

We use this because I was not able to find a good direct way in Coq to force normalization of large Church trees, because Eval compute will attempt to print the results, which has very large irrelevant overheads.

You can get around this in a couple of ways. You can do Eval compute let _ := <large tree> in tt (works for compute, vm_compute, native_compute, cbv, does not work well for lazy, simpl, cbn). You can do Definition foo := Eval compute in <large tree>. You can do Goal True. let x := eval compute in (<large tree>) in idtac. Abort. You can can also use a VM or native cast in eq_refl checking, which will cause Coq to fully normalize the type (on both sides, so you are actually measuring 4x normalization time, probably), e.g., let x := <large tree> in eq_refl x <: x = x or let x := <large tree> in eq_refl x <<: x = x (the former is a VM cast, the latter is a native cast).

[AndrasKovacs]

Thanks for the suggestions!

• Eval compute let _ := <large tree> in tt: this fails to parse with Coq 8.10. It works though as Eval compute in (let _ := t2M in tt)., but this returns instantly.
• Goal True. let x := eval compute in (<large tree>) in idtac. Abort. This seems to work.
• Definition foo := Eval compute in <large tree>: this is several times slower than the previous solution. Do you know why?

native_compute fails on my computer with the following. I have ocaml and ocaml-findlib from apt. Haven't yet bothered to repair this, along with opam, which seems broken on my system and fails to install ocaml.

File "/tmp/Coq_native32e5ff.native", line 1, characters 5-17:
Error: Unbound module Nativevalues
File "./Bench.v", line 68, characters 0-38:
Error: Native compiler exited with status 2

BTW, the reason I even have a working recent Coq is your apt build repository, thanks a lot for that!

Also, the tree normalizations are all slightly slower with your Eval compute suggestion, than with my inductive tree conversion. I find this a bit weird.

[JasonGross]

• Eval compute let _ := <large tree> in tt: this fails to parse with Coq 8.10. It works though as Eval compute in (let _ := t2M in tt)., but this returns instantly.

Ah, yes, I made a typo. The "in" after compute is important (the parentheses are not).

• Definition foo := Eval compute in <large tree>: this is several times slower than the previous solution. Do you know why?

Probably it spends time hashconsing the term. The other two possibilities are that just retypechecking the term is slow (when you make a definition, the kernel has to retypecheck the term) or that it's doing something else strange I'm not aware of.

native_compute fails on my computer with the following. I have ocaml and ocaml-findlib from apt. Haven't yet bothered to repair this, along with opam, which seems broken on my system and fails to install ocaml.

File "/tmp/Coq_native32e5ff.native", line 1, characters 5-17:
Error: Unbound module Nativevalues
File "./Bench.v", line 68, characters 0-38:
Error: Native compiler exited with status 2

BTW, the reason I even have a working recent Coq is your apt build repository, thanks a lot for that!

Glad to hear! Did you also install libcoq-ocaml-dev? That might be needed for native_compute. (I'll also note that my apt packages are not especially production-ready.). Note that the OCaml in PATH needs to be the same one that compiled Coq (this should be true if you installed OCaml from my apt ppa as well). Btw, if you want to get a working opam, you can back up ~/.opam, then delete the directory, and then install opam via the curl command on their website.

Also, the tree normalizations are all slightly slower with your Eval compute suggestion, than with my inductive tree conversion. I find this a bit weird.

This is probably because the inductive conversion doesn't need to store the entire datastructure in memory. You can probably get the speedup back by defining a fixedpoint that walks the tree and consumes it, and then Eval compute in that. For example, if the tree were a nat, you could write Fixpoint consume (n : Nat) := match n with 0 => tt | S n => consume n end.. This trick also allows you to normalize much larger terms before hitting stack overflows.

[JasonGross]

• Eval compute let _ := <large tree> in tt: this fails to parse with Coq 8.10. It works though as Eval compute in (let _ := t2M in tt)., but this returns instantly.

I forgot to address the "returns instantly" bit. It's possible there's a special optimization for unused let binders. Does the same thing happen with vmcompute? What about if you use `(fun => tt) t2M`?

[AndrasKovacs]

It happens with vm_compute and also with fun.

[JasonGross]

Oh, are these HOAS trees? The cbv strategies won't normalize under binders until the very end, so if most of the computation ends up under a binder, and then the tree disappears due to being unused, then it'll never happen.

[AndrasKovacs]

Tried opam again, opam init throws the following:

#=== ERROR while compiling ocaml-system.4.05.0 ================================#
# context     2.0.7 | linux/x86_64 |  | https://opam.ocaml.org#6e231dfd
# path        ~/.opam/default/.opam-switch/build/ocaml-system.4.05.0
# command     ~/.opam/opam-init/hooks/sandbox.sh build ocaml gen_ocaml_config.ml
# exit-code   1
# env-file    /tmp/opam-xxx-28793/ocaml-system-28793-ad6566.env
# output-file /tmp/opam-xxx-28793/ocaml-system-28793-ad6566.out
### output ###
# Unknown option --new-session

This is the usual error that I get. I was not able to get useful information about this the last time I tried, perhaps you know what's happening. The issue is perhaps an old opam installation, which infected my system in some way, despite my efforts to purge it.

[JasonGross]

According to https://github.com/ocaml/opam/issues/3424#issuecomment-425030414, you either need an updated version of bwrap, or you need to do opam init --disable-sandboxing --reinit. (I only skimmed that issue; there might be more instructions further down that issue that I missed.)