search

SkySkimmer / coq-ltac2-compiler

GNU Lesser General Public License v2.1
5 stars 0 forks source link

Compilation produces code in incorrect order #17

Closed Janno closed 12 months ago

Janno commented 1 year ago

I've found a particularly confusing bug and it took me a while to minimize and reproduce. Luckily the effort paid off. I think the bug is in evaluation order but I can only reproduce it with Ltac2 externals that manipulate global state, not with Ltac2's own mutable references so I am not entirely sure how about what's happening.

Please have a look at https://github.com/Janno/ltac2-compiler-bug-repro. I've only tested the code with 8.18 but I hope it still works with master. dune build should build everything. I didn't manage to write a working _CoqProject file so stepping through it in emacs doesn't work.

The code exposes a OCaml reference to an integer that is incremented and decremented in a stack-like fashion (i.e. decrementing only works if the argument provided is the result of the last increment). The problem is in Ltac2 test2. In > [ ... | .. push ..], the push is executed before the tactic for the first subgoal is finished. This can be prevented by adding a printf before push, as is done in Ltac2 test1.

SkySkimmer commented 12 months ago

I fixed by adding some thunking but I'm not certain it ended up correct.

It could also be argued that the externals are where the thunking should be and the compiler was correct (ie a principle that externals should always thunk before interacting with mutation). Not sure if that makes sense for your original case.

Janno commented 12 months ago

It could also be argued that the externals are where the thunking should be and the compiler was correct (ie a principle that externals should always thunk before interacting with mutation). Not sure if that makes sense for your original case.

I am not sure I understand. None of the externals in the reproducing example have side effects without being applied to arguments.

Or are you saying that a valid model would be to not expect [ a | b] to induce a fixed evaluation order between a and b?

SkySkimmer commented 12 months ago

I'm not sure TBH

SkySkimmer commented 12 months ago

But somehow something like let push () = Proofview.(Notations.(tclUNIT () >>= fun () -> state := 1 + !state; tclUNIT !state)) (or equivalently use tclLIFT) feels more correct

Janno commented 12 months ago

I fixed by adding some thunking but I'm not certain it ended up correct.

Just to make this explicit: your change fixed the problem in my original use case. I can now compile our entire automation and, as described in https://github.com/SkySkimmer/coq-ltac2-compiler/pull/21#issuecomment-1839012700, the compiler definitely helps with the runtime.

Janno commented 12 months ago

But somehow something like let push () = Proofview.(Notations.(tclUNIT () >>= fun () -> state := 1 + !state; tclUNIT !state)) (or equivalently use tclLIFT) feels more correct

I honestly think the use of thaw is just wrong in the current ltac2 code. It basically implies an invariant saying that all values of type closure have no side effects when applied. Or maybe just those that take unit arguments. It makes very little sense to me.