[declare] [tactics] Move declare to vernac

[ejgallego]

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
• moved abstract to vernac; as for now it is almost a vernacular command
• 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.

We also remove declare_private_constant from the public API.
This is an internal function for scheme declaration handled properly
now, we can also remove pure_definition_entry which is IMO good too.

This partially supersedes #10951 for now and helps with #11492 .

[ppedrot]

I am fine with most of this PR, but I'd prefer having abstract.ml still living with tactics. The fact that it relies currently on upper features is an implementation artifact that can be solved in more principled ways. By no means it is a command, otherwise you lose most of its usecases. You should use a hook instead for the time being.

[Zimmi48]

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 would make me cringe.

[ejgallego]

This would make me cringe.

Why? I'd bet I could move it there and nobody would realize for years.

Eauto and Class_tactics are not used by Coq so indeed I'm not sure what's the point of linking them in as "dead" modules instead of adding them a non-linked lib.

[SkySkimmer]

ltac is about the ltac language, not the tactics accessed through it.
Basically if it would still be relevant after moving to ltac2 only, then it shouldn't be in ltac.

[ejgallego]

I am fine with most of this PR, but I'd prefer having abstract.ml still living with tactics. The fact that it relies currently on upper features is an implementation artifact that can be solved in more principled ways. By no means it is a command, otherwise you lose most of its usecases. You should use a hook instead for the time being.

I think the problem here is that tactics placement below vernac is incorrect, as discussed in other PRs. First, quite a few tactics there are dead-ends not used by anything so they wouldn't be linked in in the first place. Second, as of today abstract for sure manipulates the "vernacular state"; so having it in tactics with a hook is a lie and won't help a lot in the long term and its type will be different for example when we move all tactics to a functional implementation.

I'd prefer to keep it in vernac as it will have to be moved anyways once a new document manager is in, so to introduce the hook as to have to move it anyways is not a lot of gain IMO. Also nobody really cares / is impacted I think. In fact, abstract should go to the independent tactic lib but the stm uses it. This is also a hack that will take a while to be amended.

[ejgallego]

ltac is about the ltac language, not the tactics accessed through it.
Basically if it would still be relevant after moving to ltac2 only, then it shouldn't be in ltac.

I agree, as of today, the ltac folder is really two components: the language, and a library of tactics. I'm all for splitting this but we need the new plugin linker. Meanwhile, I think removing -linkall outweighs the downsides, which so far seem zero to me.

[ppedrot]

First, quite a few tactics there are dead-ends not used by anything so they wouldn't be linked in in the first place

This is a technical concern unrelated to the matter at hand, and this should be considered an OCaml bug rather than anything else.

Second, as of today abstract for sure manipulates the "vernacular state"; so having it in tactics with a hook is a lie and won't help a lot in the long term and its type will be different for example when we move all tactics to a functional implementation.

It is somewhat easy to implement abstract purely functionally, without having to rely on workarounds that seem to me about as hackish, like trusted let-bindings or whatnot. We should simply thread the safe environment in the tactic monad, but the main issue is that there are a few places that escape this monad in an uncontrolled way (amongst other the pretyper).

In fact, abstract should go to the independent tactic lib but the stm uses it. This is also a hack that will take a while to be amended.

Please don't move tactic after vernac, this is nonsense, and let's collectively pretend there is no problem by using a hook. It's a pious lie, and we shouldn't base our source code organization on current defects in the implementation.

[ejgallego]

This is a technical concern unrelated to the matter at hand, and this should be considered an OCaml bug rather than anything else.

How is that an OCaml bug, if so, we should report it upstream.

Please don't move tactic after vernac, this is nonsense, and let's collectively pretend there is no problem by using a hook. It's a pious lie, and we shouldn't base our source code organization on current defects in the implementation.

The thing is that what you propose is already non possible, as a matter of fact a large bunch of tactics do effectively lie after vernac [which itself is not a single component but two]. The fact that a few tactics are in tactics and the rest scattered in other parts of the system is mostly a kinda of random setup after all the years of development.

Still, the way I see is that having a hook has significant downside, in particular it makes impossible to reason about a component in a local way; it also makes impossible to use libraries as libraries.

On the other hand, placing the tactics after the components they are using have no downsides, otherwise we would be all in some kind of large pain as this is already the case for a lot of tactics and plugins.

[ejgallego]

It is somewhat easy to implement abstract purely functionally, without having to rely on workarounds that seem to me about as hackish, like trusted let-bindings or whatnot. We should simply thread the safe environment in the tactic monad, but the main issue is that there are a few places that escape this monad in an uncontrolled way (amongst other the pretyper).

Actually after giving it a go I'm afraid this doesn't seem to be the case; abstract as specified will still have to rely on what we consider Declare internals so I'm not sure there is an easy way to do that. The hook would have to stay for a long time.

I don't think trusted let bindings are a such of a hack, they have many uses (for example finer-grain interaction with smt solvers etc...] and I have implemented them in other compiler just OK. Compared to the overhead we get with side-effects in terms of code they seem pretty clean to me, not to say the kernel already has a hack in place for them as side effects have to get inlined in a lot of cases anyways.

[ejgallego]

This should be ready; I've kept Abstract in tactics with a hook as I don't see a point holding this important PR for that discussion; I still think my comments do apply tho.

[ppedrot]

How is that an OCaml bug, if so, we should report it upstream.

The current linking strategy is all-or-nothing. We should be able to specify that some parts of the code should be linked despite the fact that they are not used. Not being able to do that seems to be a huge liability against the Coq use case, i.e. a program that features entry points to be used by plugins but not used in the program itself.

[ejgallego]

The current linking strategy is all-or-nothing. We should be able to specify that some parts of the code should be linked despite the fact that they are not used. Not being able to do that seems to be a huge liability against the Coq use case, i.e. a program that features entry points to be used by plugins but not used in the program itself.

I think part of this is due to our own linker lacking some features, I should have a new linker ready soon so we can see what is worth reporting upstream.

[ppedrot]

I'll leave a bit of time before merging in case some other reviewer wants to chime in.