-
Notifications
You must be signed in to change notification settings - Fork 0
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Compilation produces code in incorrect order #17
Comments
Fix #17 I am not fully sure that this is a compiler bug as the ~~~ocaml let l = List.map (fun f -> Proofview.tclIGNORE (thaw f)) l in ~~~ in the implementation of `dispatch` could also be blamed for not thunking properly (ie should be ~~~ocaml let l = List.map (fun f -> tclUNIT () >>= fun () -> tclIGNORE (thaw f)) l in ~~~ ) but it does seem hard or impossible to trigger a bug with non compiled ltac2.
Fix #17 I am not fully sure that this is a compiler bug as the ~~~ocaml let l = List.map (fun f -> Proofview.tclIGNORE (thaw f)) l in ~~~ in the implementation of `dispatch` could also be blamed for not thunking properly (ie should be ~~~ocaml let l = List.map (fun f -> tclUNIT () >>= fun () -> tclIGNORE (thaw f)) l in ~~~ ) but it does seem hard or impossible to trigger a bug with non compiled ltac2. This change does cause some slowdown (bug_10107 goes from 0.04s to 0.06s, non compiled baseline being 0.25s)
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. |
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 |
I'm not sure TBH |
But somehow something like |
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 #21 (comment), the compiler definitely helps with the runtime. |
I honestly think the use of |
otherwise it can be quite footgunny (even though it's hard to get a visible bug without the ltac2 compiler), for instance the current implementation of Array.set is incorrect without this. See also SkySkimmer/coq-ltac2-compiler#17 and https://coq.zulipchat.com/#narrow/stream/278935-Ltac2/topic/thunking.20and.20.60thaw.60
otherwise it can be quite footgunny (even though it's hard to get a visible bug without the ltac2 compiler), for instance the current implementation of Array.set is incorrect without this. See also SkySkimmer/coq-ltac2-compiler#17 and https://coq.zulipchat.com/#narrow/stream/278935-Ltac2/topic/thunking.20and.20.60thaw.60 Close coq#18631
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 ..]
, thepush
is executed before the tactic for the first subgoal is finished. This can be prevented by adding aprintf
beforepush
, as is done inLtac2 test1
.The text was updated successfully, but these errors were encountered: