Emilio Jesús Gallego Arias (Oct 20 2022 at 21:42): Emilio Jesús Gallego Arias (Oct 20 2022 at 21:42):Is it intended that the AST of regular tactics explodes in size once I load Ltac2?
Gaëtan Gilbert (Oct 20 2022 at 21:58):How do you measure size?
Emilio Jesús Gallego Arias (Oct 20 2022 at 22:43):I compare for example induction n after and before, I measure it with the AST printer
Emilio Jesús Gallego Arias (Oct 20 2022 at 22:44):that's for example simpl.
Emilio Jesús Gallego Arias (Oct 20 2022 at 22:44): ((CoqAst
((control ()) (attrs ())
(expr
(VernacExtend (VernacLtac2 0)
((GenArg raw (OptArg (ExtraArg ltac_selector)) ())
(GenArg raw (ExtraArg ltac2_expr)
(CTacLet false
(((CPatVar (Name (Id cl)))
(CTacCst
(AbsKn
(Other
(KerName (MPfile (DirPath ((Id Init) (Id Ltac2)))) (Id None))))))
((CPatVar (Name (Id pl)))
(CTacCst
(AbsKn
(Other
(KerName (MPfile (DirPath ((Id Init) (Id Ltac2)))) (Id None))))))
((CPatVar (Name (Id s)))
(CTacRec
(((AbsKn
(KerName (MPfile (DirPath ((Id Std) (Id Ltac2)))) (Id rBeta)))
(CTacCst
(AbsKn
(Other
(KerName (MPfile (DirPath ((Id Init) (Id Ltac2))))
(Id true))))))
((AbsKn
(KerName (MPfile (DirPath ((Id Std) (Id Ltac2))))
(Id rMatch)))
(CTacCst
(AbsKn
(Other
(KerName (MPfile (DirPath ((Id Init) (Id Ltac2))))
(Id true))))))
((AbsKn
(KerName (MPfile (DirPath ((Id Std) (Id Ltac2)))) (Id rFix)))
(CTacCst
(AbsKn
(Other
(KerName (MPfile (DirPath ((Id Init) (Id Ltac2))))
(Id true))))))
((AbsKn
(KerName (MPfile (DirPath ((Id Std) (Id Ltac2))))
(Id rCofix)))
(CTacCst
(AbsKn
(Other
(KerName (MPfile (DirPath ((Id Init) (Id Ltac2))))
(Id true))))))
((AbsKn
(KerName (MPfile (DirPath ((Id Std) (Id Ltac2)))) (Id rZeta)))
(CTacCst
(AbsKn
(Other
(KerName (MPfile (DirPath ((Id Init) (Id Ltac2))))
(Id true))))))
((AbsKn
(KerName (MPfile (DirPath ((Id Std) (Id Ltac2))))
(Id rDelta)))
(CTacCst
(AbsKn
(Other
(KerName (MPfile (DirPath ((Id Init) (Id Ltac2))))
(Id true))))))
((AbsKn
(KerName (MPfile (DirPath ((Id Std) (Id Ltac2))))
(Id rConst)))
(CTacCst
(AbsKn
(Other
(KerName (MPfile (DirPath ((Id Init) (Id Ltac2)))) (Id []))))))))))
(CTacApp
(CTacRef
(AbsKn
(TacConstant
(KerName (MPfile (DirPath ((Id Std) (Id Ltac2)))) (Id simpl)))))
((CTacRef (RelId (Ser_Qualid (DirPath ()) (Id s))))
(CTacRef (RelId (Ser_Qualid (DirPath ()) (Id pl))))
(CTacApp
(CTacRef
(AbsKn
(TacConstant
(KerName (MPfile (DirPath ((Id Notations) (Id Ltac2))))
(Id default_on_concl)))))
((CTacRef (RelId (Ser_Qualid (DirPath ()) (Id cl))))))))))
(GenArg raw (ExtraArg ltac_use_default) false)))))))))
induction is even worse (including extension objects, by the way, Yet Another Custom Imperative Extension System in Ltac2, yay!)
Emilio Jesús Gallego Arias (Oct 20 2022 at 22:46):that's the regular case, not the IDEs can make much sense of it either
Emilio Jesús Gallego Arias (Oct 20 2022 at 22:46):CoqAst
((control ()) (attrs ())
(expr
(VernacExtend (VernacSolve 0)
((GenArg raw (OptArg (ExtraArg ltac_selector)) ())
(GenArg raw (OptArg (ExtraArg ltac_info)) ())
(GenArg raw (ExtraArg tactic)
(TacAtom
(TacReduce
(Simpl
((rBeta true) (rMatch true) (rFix true) (rCofix true)
(rZeta true) (rDelta true) (rConst ()))
())
((onhyps (())) (concl_occs AllOccurrences)))))
(GenArg raw (ExtraArg ltac_use_default) false)))))))))
This looks like the output of the Ltac2 AST, not the Ltac1 AST. Importing Ltac2 module sets by default the proof mode to the Ltac2 one, so when you write induction n you get the expansion of the induction n Ltac2 notation.
Pierre-Marie Pédrot (Oct 21 2022 at 06:30):Missing input: Ltac 2 macro expansion is performed at parsing time. You could probably try to move it somewhere else but it would complicate the implementation and add the temptation to have macros doing more than macros.
Pierre-Marie Pédrot (Oct 21 2022 at 06:32):including extension objects
What are you talking about? Ltac2 uses Libobject as intended, and the "imperative" registering commands are just like all the other ones in Coq, i.e. static registering. This doesn't qualify as imperative.
Enrico Tassi (Oct 21 2022 at 07:48):As if imperative had a negative connotation in the real world... :thinking:
Emilio Jesús Gallego Arias (Oct 21 2022 at 08:01):Pierre-Marie Pédrot said:
Missing input: Ltac 2 macro expansion is performed at parsing time. You could probably try to move it somewhere else but it would complicate the implementation and add the temptation to have macros doing more than macros.
Yup, that's ltac2 AST, indeed having parsing do macro expansion is not so bad, however it is surprising how large the terms do become, it seems to carry some kind of env? How does the printer handle them (I can look at the code too hehe)
What are you talking about? Ltac2 uses Libobject as intended, and the "imperative" registering commands are just like all the other ones in Coq, i.e. static registering. This doesn't qualify as imperative.
I mean Tac2dyn, that's imperative in the sense that calls to create tags are. This is indeed a similar problem that the rest of generic args, but makes for example defining custom parsers, hash functions, etc... [which are needed in my context] a manual prone-to-error process; in particular the plugin programmer has to find all the tags by hand and keep its own database. It would be nice if we could have a more systematic interface for the plugins willing to consume this kind of extensible AST
Enrico Tassi (Oct 21 2022 at 09:15):Emilio Jesús Gallego Arias said:
Pierre-Marie Pédrot said:
Missing input: Ltac 2 macro expansion is performed at parsing time. You could probably try to move it somewhere else but it would complicate the implementation and add the temptation to have macros doing more than macros.
This is indeed a similar problem that the rest of generic args, but makes for example defining custom parsers, hash functions, etc... [which are needed in my context] a manual prone-to-error process; in particular the plugin programmer has to find all the tags by hand and keep its own database. It would be nice if we could have a more systematic interface for the plugins willing to consume this kind of extensible AST
IMO you should make the hash function part of the contract when one registers a new argument, as the pretty printer is. This has nothing to do with being imperative. It is just that the API does not fit your needs.
Emilio Jesús Gallego Arias (Oct 21 2022 at 19:23):Imperative in this case means both that it is not possible to determine using the type system whether a module registers stuff (and what), and that undoing such effects is not often not possible or hard. This is fatal when using common programming patterns such as incremental computation based on immutable data structures, to name one. But yes, the API is also quite hard to use (tho it can be tamed as serlib does), very hard to maintain (need to have a huge test suite), and your proposal doesn't work as often one needs for example several / different hashing functions depending on the use case.
Going back on topic, I'm now convinced the Ltac2 AST is very strange, for many definitions of what people expect an AST to be. Looking at what is produced at parsing simpl for example, the locations doesn't make a lot of sense on the very large expression produced by the expansion.
Gaëtan Gilbert (Oct 21 2022 at 20:14):Pierre-Marie Pédrot said:
Missing input: Ltac 2 macro expansion is performed at parsing time. You could probably try to move it somewhere else but it would complicate the implementation and add the temptation to have macros doing more than macros.
we probably should move it to a separate phase tbh
Pierre-Marie Pédrot (Oct 21 2022 at 21:56):undoing such effects is not often not possible or hard
That's the point about being static: there is not point in undoing them.
Pierre-Marie Pédrot (Oct 21 2022 at 22:00):(I will revise my position when OCaml lets you unlink dynlinked code. Until then...)
Emilio Jesús Gallego Arias (Oct 25 2022 at 18:52):Pierre-Marie Pédrot said:
(I will revise my position when OCaml lets you unlink dynlinked code. Until then...)
Not related to this discussion but I'm bitten by this pretty often due to the parser (there is a bug open) , like load ssreflect, unload it, then paste a different file, pum, need to restart coq-lsp (or coqtop)
Anyways the immediate use case I was thinking at hand is the new printer that jsCoq is trying to do, it is a bit painful to implement something like that with the current way the AST is setup. A different issue is how radically Ltac1 proofs did change when you import ltac2
Last updated: Oct 12 2024 at 13:01 UTC