Skip to content
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

Open
01mf02 opened this issue Jul 7, 2022 · 7 comments
Open

Backwards compatibility #2

01mf02 opened this issue Jul 7, 2022 · 7 comments
Labels

Comments

@01mf02
Copy link
Collaborator

01mf02 commented Jul 7, 2022

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.

@fblanqui
Copy link
Member

fblanqui commented Jul 7, 2022

I agree. Changing the syntax requires to change tools. So changes in the syntax should come with some pull requests on tools.

@01mf02
Copy link
Collaborator Author

01mf02 commented Jul 7, 2022

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?

@francoisthire
Copy link
Collaborator

francoisthire commented Jul 8, 2022

we will not have to write a syntax converter and so on.

Am I wrong, but since we have at least two parsers, a breaking change could be adapted so that:

  1. We need to write/modify each parser (but this is kind of independent of the breaking change). The complexity of it depends on the modification.
  2. We can write a converter: a) Copy/Paste the current parser b) Write a printer for the new syntax.
  3. Apply the converter on demand, or at the beginning, include it directly with the tools wanted to read the standard

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.

@francoisthire francoisthire mentioned this issue Jul 8, 2022
@francoisthire
Copy link
Collaborator

Another argument I would like to make in favor of a breaking change is:

  • If we want to be a standard, we need to ease people of using it (either by writing parsers for it/or printer towards it). If we need only a single breaking change to satisfy this, I suppose we should. We are not writing a standard for the 10 people involved, but also for the next 700 people to come ;)

@01mf02
Copy link
Collaborator Author

01mf02 commented Jul 15, 2022

I can see your reasoning, @francoisthire.

If we want to be a standard, we need to ease people of using it

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? ...
And where do you think these people struggle today?

@01mf02
Copy link
Collaborator Author

01mf02 commented Jul 15, 2022

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.

@francoisthire
Copy link
Collaborator

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:

  • Read files written in the standard
  • Write files for the standard
  • Interpret files

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 dk to parse strictly the standard. However, they need to have a way to print files into this standard. This could allow for example to not annotate every abstraction. But if the standard requires it, then dk needs to have a mode to print annotation for every abstraction.

Hence dk can still be convenient to use while being compliant with the standard.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

3 participants