-
Notifications
You must be signed in to change notification settings - Fork 645
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
[tactics] [rfc] Move ltac-specific tactics to ltac. #10951
Conversation
f745f4a
to
b7881ef
Compare
b7881ef
to
b493126
Compare
CI seems broken. |
In the current situation, I disagree with this change. The tactics that you are moving are not Ltac1-specific, so moving them to the Ltac plugin would only lead to code duplication, or creating a dependency of Ltac2 on Ltac1 (which is the solution adopted in this PR). Both solutions are bad. Code duplication leads to slow divergence, with inconsistent behaviors that go mostly unnoticed but can lead to confusion (and wrong documentation). Creating such dependency would make it more complicated to deprecate Ltac1 in the future. Overall, while versioning tactics might be a good idea, I really do not see how hard linking tactic versioning with the version of the tactic language is going to make the transition easier, on the contrary. Of course, I may very well be wrong, and I am fully open to hearing arguments that make me change my mind about this. |
Actually, I agree with @Zimmi48. There is no such thing as "Ltac-specific tactic" othewise you better move the whole pretyper to the Ltac folder. |
Indeed, I moved them to LTAC as to avoid creating another plugin. Note tho that for example |
b493126
to
042c445
Compare
042c445
to
bc1b1d0
Compare
This PR is a draft to request for more comments, likely far from final form yet. See issue coq#9547 This is also related to PR coq#10951 and coq#7698 We seem to save half to one megabyte in the binaries: ``` -rwxr-xr-x 1 egallego egallego 31651662 janv. 31 00:05 coqc_bin.bc -rwxr-xr-x 1 egallego egallego 32467231 janv. 31 00:08 coqc_bin.bc -rwxr-xr-x 1 egallego egallego 23781840 janv. 31 00:05 coqc_bin.exe -rwxr-xr-x 1 egallego egallego 24395352 janv. 31 00:08 coqc_bin.exe -rwxr-xr-x 1 egallego egallego 23751520 janv. 31 00:05 coqtop_bin.exe -rwxr-xr-x 1 egallego egallego 24395608 janv. 31 00:08 coqtop_bin.exe -rwxr-xr-x 1 egallego egallego 41996191 janv. 31 00:05 coqtop_byte_bin.bc -rwxr-xr-x 1 egallego egallego 43020328 janv. 31 00:08 coqtop_byte_bin.bc ```
This PR is a draft to request for more comments, likely far from final form yet. See issue coq#9547 This is also related to PR coq#10951 and coq#7698 We seem to save half to one megabyte in the binaries: ``` -rwxr-xr-x 1 egallego egallego 31651662 janv. 31 00:05 coqc_bin.bc -rwxr-xr-x 1 egallego egallego 32467231 janv. 31 00:08 coqc_bin.bc -rwxr-xr-x 1 egallego egallego 23781840 janv. 31 00:05 coqc_bin.exe -rwxr-xr-x 1 egallego egallego 24395352 janv. 31 00:08 coqc_bin.exe -rwxr-xr-x 1 egallego egallego 23751520 janv. 31 00:05 coqtop_bin.exe -rwxr-xr-x 1 egallego egallego 24395608 janv. 31 00:08 coqtop_bin.exe -rwxr-xr-x 1 egallego egallego 41996191 janv. 31 00:05 coqtop_byte_bin.bc -rwxr-xr-x 1 egallego egallego 43020328 janv. 31 00:08 coqtop_byte_bin.bc ```
This PR is a draft to request for more comments, likely far from final form yet. See issue coq#9547 This is also related to PR coq#10951 and coq#7698 We seem to save half to one megabyte in the binaries: ``` -rwxr-xr-x 1 egallego egallego 31651662 janv. 31 00:05 coqc_bin.bc -rwxr-xr-x 1 egallego egallego 32467231 janv. 31 00:08 coqc_bin.bc -rwxr-xr-x 1 egallego egallego 23781840 janv. 31 00:05 coqc_bin.exe -rwxr-xr-x 1 egallego egallego 24395352 janv. 31 00:08 coqc_bin.exe -rwxr-xr-x 1 egallego egallego 23751520 janv. 31 00:05 coqtop_bin.exe -rwxr-xr-x 1 egallego egallego 24395608 janv. 31 00:08 coqtop_bin.exe -rwxr-xr-x 1 egallego egallego 41996191 janv. 31 00:05 coqtop_byte_bin.bc -rwxr-xr-x 1 egallego egallego 43020328 janv. 31 00:08 coqtop_byte_bin.bc ```
This could be seen as a plan to make `tactics` independent of `vernac`, also it could facilitate the versioning of tactics by packing them. Remaining non-core tactics in `tactics` have to remain there due to scheme declaration. Moving scheme declaration higher would allow us to move the tactics too. This PR is a Request for Comments, I am myself not pushing this idea strongly, feedback welcome. Doing a `Tactics_v8` pack could be another choice for example.
bc1b1d0
to
9028a9d
Compare
I don't know about the relation to #11492, but as said above, I don't think Incidentally, for a change, it is not me but a user who was complaining today at my table about the lack of unity between tactics. This should be one of our priority :) |
I think that virtually all comments in this thread are in favour of not merging this PR. Should we close it, @ejgallego ? |
@ppedrot sorry I missed your comment; I propose we discuss this in the next call. While this PR may not be the proper solution, the problems still remains:
I'm all for creating a proper library for tactics, which could be dynamically loaded if you want, I did this PR with the idea of at least uniformizing dependencies. So indeed maybe the right move would be to split the tactics directory. I did a quick check and indeed "core" tactics are almost not used in the rest of Coq as this PR points out except for scheme generation, that is to say, it is feasible to move all core tactics to a plugin and still get a building |
If you want to think of it that way; the motivation for this PR was towards improving modularization; the main benefit I would see from that would be to have indeed different tactic libraries for compat purposes for example. |
Basically, the tactics and the tactic language are two mostly independent things. The tactic language (through the proof mode) only determines the syntax with which tactics must be called. |
Note that I wouldn't mind putting tactics in their own plugin, that both Ltac1 and Ltac2 would depend on. However, creating an artificial dependency of Ltac2 on Ltac1 is a big no. And the fact that this dependency already exists today (according to the META file) is no excuse: this dependency should be cut off ASAP and certainly not reinforced. |
Don't we need one to depend on the other to provide interop?
Gaëtan Gilbert
…On 02/02/2020 20:33, Théo Zimmermann wrote:
Note that I wouldn't mind putting tactics in their own plugin, that both
Ltac1 and Ltac2 would depend on. Creating an artificial dependency of
Ltac2 on Ltac1 is a big no. And the fact that this dependency already
exists today (according to the META file) is no excuse: this dependency
should be cut off ASAP and certainly not reinforced.
—
You are receiving this because you commented.
Reply to this email directly, view it on GitHub
<#10951?email_source=notifications&email_token=AASZB3DA6MFW777LDDLZJXTRA4NZDA5CNFSM4JEYTQ22YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOEKR64VI#issuecomment-581168725>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AASZB3DMT4B6BZGIOZFLUJLRA4NZDANCNFSM4JEYTQ2Q>.
|
@SkySkimmer this can be done via a third plugin above both Ltac2 and Ltac1. Currently the code for compability is part of Ltac2, but that was done mostly out of easiness. |
BTW I strongly oppose moving this code to a plugin until it's easier to debug. Hopefully ocaml 4.10 will help with that. |
Could be a "plugin" [that is to say, a library] which lives above toplevel but it is always linked in. |
Currently, my own experience is that I can step in plugins (after a static link of them) but, under Emacs, because of the "packing", the Emacs camldebug mode is not able to compute what need to be sent to |
Discussion result is that we will still move the ununused tactics to their own library, but below ltac. The library will be statically linked at least until we implement a better dynamic linker / ocamldebug can handle it. This however poses a problem for removing |
I will defer this until Dune is the default build system. |
@ejgallego I propose closing this in the meantime, please reopen when that happens. |
Keeping it open as otherwise once the ref is modified PRs cannot be reopened. |
This PR moves `Declare` to `vernac` which will hopefully allow to unify it with `DeclareDef` and avoid exposing entry internals. There are many tradeoffs to be made as interface and placement of tactics is far from clear; I've tried to reach a minimally invasive compromise: - moved leminv to `ltac_plugin`; this is unused in the core codebase and IMO for now it is the best place - hook added for abstract; this should be cleaned up later - hook added for scheme declaration; this should be cleaned up later - separation of hints vernacular and "tactic" part should be also done later, for now I've introduced a `declareUctx` module to avoid being invasive there. In particular this last point strongly suggest that for now, the best place for `Class_tactics` would be also in `ltac`, but I've avoided that for now too. This partially supersedes coq#10951 for now and helps with coq#11492 .
This PR moves `Declare` to `vernac` which will hopefully allow to unify it with `DeclareDef` and avoid exposing entry internals. There are many tradeoffs to be made as interface and placement of tactics is far from clear; I've tried to reach a minimally invasive compromise: - moved leminv to `ltac_plugin`; this is unused in the core codebase and IMO for now it is the best place - hook added for abstract; this should be cleaned up later - hook added for scheme declaration; this should be cleaned up later - separation of hints vernacular and "tactic" part should be also done later, for now I've introduced a `declareUctx` module to avoid being invasive there. In particular this last point strongly suggest that for now, the best place for `Class_tactics` would be also in `ltac`, but I've avoided that for now too. This partially supersedes coq#10951 for now and helps with coq#11492 .
I believe, and judging from the discussions, I am not the only one, that the fix implemented by this PR is dead wrong. Given that:
it doesn't seem far-fetched that we should close this PR and reopen a fresh one with the correct fix when it exists. It is not even clear what is the best course of action, but likely an intermediate plugin compiled with linkall. |
We could now do this thanks to #15220 , by putting these tactics in a library that ocamlfind knows how to load when ltac is loaded. However as we are stuck with linkall, not so much motivation to do it then. |
This could be seen as a plan to make
tactics
independent ofvernac
, also it could facilitate the versioning of tactics bypacking them.
Remaining non-core tactics in
tactics
have to remain there due toscheme declaration. Moving scheme declaration higher would allow us to
move the tactics too.
This PR is a Request for Comments, I am myself not pushing this idea
strongly, feedback welcome. Doing a
Tactics_v8
pack could be anotherchoice for example.