[experiment] Get Ltac2 working without coq stdlib

[Alizter]

trafficstars

This was an attempt to get Ltac2 working without the coq stdlib. There are however a lot of anomalies however. I suspect we are shedding light on some Ltac2 issues as a result.

In Syllepsis.v, even after removing all parts of the Ltac2 library that cause anomalies, the actual Ltac2 decelerations are raising anomalies. I will need to debug further with some experts.

This is not as simple as getting Ltac2 to compile with noinit since it needs to reference Ltac1 in some places. But we don't share the Ltac1 decelerations with the coq stdlib. I have therefore opted for our tried and tested method of copying the coq stdlib and removing as little as possible to get it to work. As you can see, after all this, there is some anomalous behaviour of Ltac2.

[Alizter]

Here is a backtrace of the anomaly:

Backtrace

Anomaly "Uncaught exception Not_found."
Please report at http://coq.inria.fr/bugs/.
Raised at Int.Map.find in file "clib/int.ml", line 39, characters 14-29
Called from HMap.Make.find in file "clib/hMap.ml", line 365, characters 12-28
Called from Ltac2_plugin__Tac2env.interp_type in file "plugins/ltac2/tac2env.ml" (inlined), line 86, characters 21-65
Called from Ltac2_plugin__Tac2intern.is_unfoldable in file "plugins/ltac2/tac2intern.ml", line 276, characters 33-57
Called from Ltac2_plugin__Tac2intern.kind in file "plugins/ltac2/tac2intern.ml", line 299, characters 5-21
Called from Ltac2_plugin__Tac2intern.unify0 in file "plugins/ltac2/tac2intern.ml", line 349, characters 33-44
Called from Ltac2_plugin__Tac2intern.unify in file "plugins/ltac2/tac2intern.ml", line 362, characters 6-22
Called from Ltac2_plugin__Tac2intern.unify_arrow.iter in file "plugins/ltac2/tac2intern.ml", line 372, characters 13-33
Called from Ltac2_plugin__Tac2intern.intern_rec in file "plugins/ltac2/tac2intern.ml", line 756, characters 12-37
Called from Ltac2_plugin__Tac2intern.intern_rec in file "plugins/ltac2/tac2intern.ml", line 725, characters 15-37
Called from Ltac2_plugin__Tac2intern.intern in file "plugins/ltac2/tac2intern.ml", line 1198, characters 15-31
Called from Ltac2_plugin__Tac2entries.register_ltac.map in file "plugins/ltac2/tac2entries.ml", line 348, characters 17-41
Called from CList.map in file "clib/cList.ml", line 430, characters 21-24
Called from Ltac2_plugin__Tac2entries.register_ltac in file "plugins/ltac2/tac2entries.ml", line 363, characters 13-33
Called from Vernacextend.vtdefault.(fun) in file "vernac/vernacextend.ml", line 136, characters 29-33
Called from Vernacinterp.interp_typed_vernac in file "vernac/vernacinterp.ml", line 20, characters 20-113
Called from Vernacinterp.interp_control.(fun) in file "vernac/vernacinterp.ml", line 207, characters 24-69
Called from Flags.with_modified_ref in file "lib/flags.ml", line 17, characters 14-17
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernacinterp.interp_gen.(fun) in file "vernac/vernacinterp.ml", line 257, characters 18-43
Called from Vernacinterp.interp_gen in file "vernac/vernacinterp.ml", line 255, characters 6-279
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Stm.Reach.known_state.reach.(fun) in file "stm/stm.ml", line 2178, characters 16-43
Called from Stm.State.define in file "stm/stm.ml", line 964, characters 6-10
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Stm.Reach.known_state.reach in file "stm/stm.ml", line 2320, characters 4-105
Called from Stm.observe in file "stm/stm.ml", line 2421, characters 4-60
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Stm.finish in file "stm/stm.ml", line 2432, characters 12-50
Called from Dune__exe__Idetop.goals in file "ide/coqide/idetop.ml", line 214, characters 13-28
Called from Dune__exe__Idetop.eval_call.interruptible in file "ide/coqide/idetop.ml", line 472, characters 12-15
Called from Xmlprotocol.abstract_eval_call in file "ide/coqide/protocol/xmlprotocol.ml", line 759, characters 29-46

[Alizter]

cc @ppedrot I suspect we are missing some registrations or something. What do you think?

[SkySkimmer]

https://github.com/coq/coq/blob/7c608fe3e9a3054c6809ae8556bea404256369c7/plugins/ltac2/tac2intern.ml#L24-L32 https://github.com/coq/coq/blob/7c608fe3e9a3054c6809ae8556bea404256369c7/plugins/ltac2/tac2env.ml#L282-L289 ie Ltac2.Init (Std, Ltac1) can't be called HoTT.Tactics.Ltac2.Init

[SkySkimmer]

There's also stuff in tac2core looking types up by name

[Alizter]

As I see it there are two choices. Either we remove these hard coded paths and replace them with a Coqlib register or we compile Ltac2 itself with noinit. I've opted for the second less destructive option since the payoff for the first isn't that great. This will let us import the standard Ltac2 library without transitively importing any Coq stdlib.

Here is Ltac2 compiled with noinit: https://github.com/coq/coq/pull/15632

Either way, at the earliest, the fix for importing Syllepsis.v will come shipped in 8.16 so probably around summer. For now we can probably live with not importing Syllepsis.v too much, and we can even add a comment warning users that the Ltac2 can cause the stdlib to be imported also.

[jdchristensen]

I think that if we can't fix this in the HoTT library right now, we should switch Syllepsis to use the Ltac1 version of the tactic. It's only 0.9s, and has other benefits, such as being easier to understand. We could switch back to the Ltac2 version in the future if it can be done in a way that avoids the stdlib. If you agree, I can create a PR for Syllepsis.v.

[Alizter]

@jdchristensen I think we can live with 0.9sec for the time being. We can always go back to the Ltac2 version from the git history also. So please go ahead and create that PR.