lambdapi
lambdapi copied to clipboard
Deducteam
Have a parsing state for handling notations defined in other modules ?
We will need to handle dependencies separately to make things work for the editor mode (or rather, LSP server) developed by @ejgallego. In particular, we need to change the way files are parsed to be able to resolve dependencies without needing to compile files at the same type.
The proposed approach is for files to start with a prelude containing all the require commands, that could be parsed beforehand, without having to care with all the syntax extension bullshit.
This is related to discussions in #178 and discussions in https://github.com/Deducteam/lambdapi/commit/ea120ef2c1fe696380d91f7823cb00b0b75216a3#commitcomment-33017724.
I can try to give this a go in the next weeks; I am more favorable towards having a parsing state tho; in the long term users want to open a notation scope so as I mentioned in the commit the prelude approach doesn't work there.
Delegating compilation is desired but not as important, IMO it can wait.
OK, then I'm not sure I understood your proposal! Can you explain a little more? I will try to find the time to work on that in the following weeks, and it would be better that we agree on the way to go before either of us start coding I guess.