@Pierre-Marie Pédrot : I have a hard time finding the term syntax for variable assignments. E.g. this doesn't work:
Ltac2 mutable x := 0.
Ltac2 Eval (Int.add 1 2).
Ltac2 Set x := 3.
Ltac2 Set x := (Int.add 1 2).
The last line fails with "Tactic definition must be a syntactical value". According to the docs this should work. Do I miss something or is this a bug?
Where does the doc say this is legal? Any toplevel definition, including "mutable" assignment, must be a value.
You need to wrap it in a thunk for this to be legal.
i.e. Ltac2 mutable x () := 0.
semantically the only reasonable way to override a definition with a non-value is from within an evaluation, but then there is https://github.com/coq/coq/pull/13982 which is stuck for some reason
having no way to evaluate and assign at top level is pretty weird for a ocaml lookalike tbh
I agree, but it is what it is.
Allowing toplevel mutability would just break everything regarding document evaluation.
You can't backtrack in an OCaml file...
you can in ocamldebug
Pierre-Marie Pédrot said:
Where does the doc say this is legal? Any toplevel definition, including "mutable" assignment, must be a value.
The error message is a bit misleading - it makes one think that it is a syntax issue and syntactically what I wrote should be allowed.
But indeed the manual says:
The body of an Ltac2 definition is required to be a syntactical value that is, a function, a constant, a pure constructor recursively applied to values or a (non-recursive) let binding of a value in a value.
The term "syntactical value" is a bit hard to grasp for me. Once evaluated a function application is also a value and it is not obvious why the Set does not evaluate its right hand side.
@Gaëtan Gilbert not fully, if you write to a file good luck backtracking on that
@Michael Soegtrop because a function can perform arbitrary effects that cannot be properly tracked at the level of the document. Imperative modification is one, but tactics can do more including local extension of the environment with constants / universes, firs-class backtrack and whatnot.
Well maybe we should have a concept of pure functions then.
What I am mostly after is a way to build up something like a hint database in a global variable. Hiding this in a thunk is performance wise not feasible because then at each use the database would be recreated.
I also don't see how https://github.com/coq/coq/pull/13982 increases the expressiveness of Ltac2. If the changes are local to a vernac, I could also use say some local state record with mutable fields. But I don't see a way to assign a complicated computed data structure to a global variable in Ltac2.
@Michael Soegtrop with that PR you can do everything as a thunk and evaluate once the value of it inside the relevant tactic, so you only have to pay once for this
currently this can be encoded in an impractical way by passing explicitly your hint database to the corresponding functions and evaluate the thunk at toplevel and pass that to the subcalls
but this is explicit, so annoying and not very modular
As for global tables, I agree that this should actually be provided by some dedicated primitive because it's a very common use case in tactics.
The catch is that one has to be careful what is stored in these tables since the same value restriction applies.
Pierre-Marie Pédrot said:
Allowing toplevel mutability would just break everything regarding document evaluation.
that's about Set, but why can't we do Ltac2 x := Int.add 1 2.
?
Hmm I must admit I don't see the advantage of using globals here. In complicated algorithmic tactics I tend to have some sort of state record I pass around anyway. How modularity can be increased by using globals I don't see.
@Gaëtan Gilbert same problem, you can't store safely a potentially mutable value inside a toplevel entry. This wreaks havoc with backtrack (and serialization).
@Michael Soegtrop well if you already abide by the reader monad it's indeed free, but it's still annoying to have to pass this explicitly
Yes it is a bit annoying, but the semantics are quite obvious and a state record makes it explicit what the state is. The main downside of the PR is that IMHO the semantics are not obvious.
If the main issue is mutability, I would really think about having pure functional types and functions. If this is the price one has to pay for mutability, I would rather go without mutable arrays and records. Some algorithms require mutable data structures but there are usually functional alternatives which are not that much worse.
Isn't this easy to detect if a function is "pure"?
E.g. I would think that using search trees instead of hash tables but building them only once is more efficient than using hash tables which need to be recomputed on each use.
The problem is not only mutability, the effects provided by the monad (e.g. the fact we have an implicit evar map floating around) is also troublesome
Essentially the fact we can evaluate a Coq document in weird ways (backtrack, parallel processing, etc.) coerces us into having to be pure at the level of the metalanguage.
You can't just implement a hashtable in Ltac2 and hope for this to magically make sense at the level of the document.
The only sane place where effects can occur are in places where no vernacular command can be tampered with, i.e. in a single Ltac2 run.
You could have a type-and-effect system but that's very heavyweight and most of the answers will be anyways "this is impure"
for instance you can't even evaluate a constr in a tactic in a meaningful way
I think you can have documents work with that, whether that's a good idea that's a different story
because this depends on the current environment, can generate evars / universes, etc.
The important thing for the document is the DAG of dependencies, now it is a bit unclear
@Emilio Jesús Gallego Arias I can't even think of a sane semantics even with all due support from the doc manager
but imagine we had it sorted out, so we can track what the mutable state needs, for example in terms of the univ map, etc...
in principle you can support mutable update of a dag node
Ltac2 references are literally OCaml references, so you'd need to track that if you allowed them inside toplevel values
you need to define indeed what preorder you wanna put on change propagation
given that you have higher order in the language it's basically hopeless
it's easy to get a loop XD
or lose as you mention referential transparency
you could give referential transparency away
but I agree maybe the sanest is not to allow it
but as in it is possible to do, it is
wut? like you backtrack and replay a proof and it says something else?
if you want to have referential transparency you need to avoid cycles on the DAG otherwise you are boom, and that's a hard problem
oh my
in any case I think this is an XY-problem
yes, that's the whole point of the mutability
what's the use case again?
defining maps of stuff at toplevel in all likeliness
I agree with you, doesn't seem a sane idea
Define them in a pure way, no?
There are API such as the one in Lean that allows you to have a functional interface, but the implementation doesn't copy
aka linearity
I think we need language support for toplevel maps, as a generalization of Hint databases
This one is sane semantically, you just keep track of the stuff in the summary / libobject as usual
Yup, you could just allow shadowing in Ltac2
So people can do Ltac2 my_map := empty.
and later on Ltac2 my_map := add foo my_map.
before shadowing we would need to allow my_map' := add foo my_map
I am not sure that a fixed top level map data structure is the solution - I am using quite different structures for different purposes.
Would it really be hopeless to have a pure subset?
Say only non mutable Ltac types and constr terms without evars?
That would be sufficient for my purposes.
Pierre-Marie Pédrot said:
for instance you can't even evaluate a constr in a tactic in a meaningful way
please explain more
What's the value if you backtrack (in the monad, I mean)? You can generate references that are captured by the continuation, for instance.
I guess you could pick the first value, but then you need to be careful to propagate the universes / evars and whatnot inside the environment.
This only makes sense for constrs, so in particular it means this should be a specific command, not some magic handling of terms inside the Ltac2 definition command.
i.e. Ltac Term foo := ...
.
(and we already have this, it's Definition foo := ltac2:(...)
.
just imagine what happens if people start storing arbitrary OCaml values in the summary, including references, functions, or worse.
we already had to introduce a dedicated support only for futures in the global environment...
(and even there it was pretty broken)
Yeah, the summary is not the right place, maybe what MIchael is facing are limitations of the proof search engine?
From a logic programming point of view, the engine is quite basic
But in my understanding, there is no free lunch here, the Coq setting is not very forgiving in that sense
using hacks such as the document are not gonna solve fundamental limitations
Last updated: Dec 07 2023 at 11:02 UTC