-
Notifications
You must be signed in to change notification settings - Fork 0
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Backwards compatibility #2
Comments
I agree. Changing the syntax requires to change tools. So changes in the syntax should come with some pull requests on tools. |
Ok, but do we want to change the syntax such that output from existing tools has to be changed? And if so, why? |
Am I wrong, but since we have at least two parsers, a breaking change could be adapted so that:
The AST of the old syntax is so simple, that writing a simple printer is a matter of some hours of work. Modifying all the tools requires more. Another advantage is, with a converter, modifying tools printing old syntax to the new one can be done incrementally which cannot be done without a converter. |
Another argument I would like to make in favor of a breaking change is:
|
I can see your reasoning, @francoisthire.
This is the interesting point for me. Who are the "users"? People writing Dedukti by hand? People exporting proofs to Dedukti? People writing tools to process Dedukti files? ... |
Speaking of myself as a developer of a Dedukti parser, I think that a simpler term syntax could have its benefits for parser developers. However, a simpler term syntax has the potential to make writing Dedukti by hand more difficult. So it's all about trade-offs. That's why it is important to know who we want to make Dedukti easier for. |
IIUC, writing manually a parser, and using libraries such as YACC or Menhir to write the parser is two different things. It is not reasonable to assume people will write a parser without writing a grammar. I think all the standard languages include a library to read a grammar and produce an automaton out of it. However, your input was important to understand the ambiguity with the current grammar and can be used to make a grammar less ambiguous, hence easier to write, and faster. A user of a standard may need to:
We need to target those three usages at the same time. Writing or modifying files written in the standard is a different usage. For example, I do not believe that being compliant with the standard requires the tools like Hence |
Are existing DK files considered to be valid "DK3 syntax"?
I believe that there is a lot of interest in keeping backwards-compatibility, notably because that means that we will not have to update proof exporters, we will not have to write a syntax converter and so on. Who wants to do such chores anyway?
However, if there is a really good point about why it is necessary to break the syntax, then I am all ears. But so far I did not hear such arguments.
The text was updated successfully, but these errors were encountered: