Skip to content
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

Closed
Janno opened this issue Dec 4, 2023 · 6 comments · Fixed by #19
Closed

Compilation produces code in incorrect order #17

Janno opened this issue Dec 4, 2023 · 6 comments · Fixed by #19

Comments

@Janno
Copy link

Janno commented Dec 4, 2023

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 added a commit that referenced this issue Dec 4, 2023
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.
SkySkimmer added a commit that referenced this issue Dec 4, 2023
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)
@SkySkimmer
Copy link
Owner

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
Copy link
Author

Janno commented Dec 4, 2023

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
Copy link
Owner

I'm not sure TBH

@SkySkimmer
Copy link
Owner

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

@Janno
Copy link
Author

Janno commented Dec 4, 2023

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 #21 (comment), the compiler definitely helps with the runtime.

@Janno
Copy link
Author

Janno commented Dec 4, 2023

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.

SkySkimmer added a commit to SkySkimmer/coq that referenced this issue Dec 19, 2023
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
SkySkimmer added a commit to SkySkimmer/coq that referenced this issue Jul 18, 2024
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants