New config syntax

Stream: metaprogramming / tactics

[Jannis Limperg]

@Kyle Miller I'm looking at how to adapt Aesop to the new config syntax (which is very nice btw). Would it be possible to get a TermElabM version of declare_config_elabor a public version of mkConfigElaborator?

(Also, should the recover field maybe move to the context of TermElabM instead of TacticM? Recovering from errors seems to me like a general elaboration concept and not something specific to tactics.)

[Kyle Miller]

Yeah, a term elab version would be possible. I just didn't see any uses of configurations that needed it, so I didn't add it. For now I'd rather not make mkConfigElaborator a public interface.

Regarding the recover state, I haven't spent time yet to fully understand what it's supposed to represent and how it's meant to be different from the TermElabM errToSorry state. I think ideally we would have a system that keeps track of whether a tactic is "interactive" or not, which has to do whether exceptions should be reported as log messages, and whether we should run diagnostics that would help a user figure out why a tactic failed.

I've had a suspicion that errToSorry could be renamed recover. That's likely incorrect, but it seems worth looking into.

[Kyle Miller]

Question though @Jannis Limperg: does Aesop need to be elaborating its configurations in TermElabM? Or would it be better to stick with TacticM, and if you do need to elaborate any terms, use Tactic.elabTerm, etc., to make sure elaboration is completed on each term individually?

[Kyle Miller]

Is it that you're running into needing to have the Aesop ruleset parser work both for attributes and tactics?

[Jannis Limperg]

I think I could lift everything in the specific file that sparked this discussion into TacticM because it only concerns the elaboration of tactic arguments. And indeed I should maybe be using Tactic.elabTerm and friends there. I currently solve any elaboration-related problems by shotgun-disabling all the advanced elaboration features. :sweat_smile:

However, there are indeed other parts of Aesop's frontend that are meant to be usable from attributes, so there TacticM wouldn't make as much sense. As far as I can tell, I could use the TacticM functions anyway and then run with an empty goal list. But this, to me, indicates that these functions shouldn't be in TacticM in the first place: they only use the recover field, not the actual goals.

[Kyle Miller]

For @[simps], the way I upgraded it was to lift the command version of the elaborator to AttrM

[Jannis Limperg]

Ah yeah, that would work as well.