Juvix to Isabelle/HOL translation

[lukaszcz]

• Closes Translate Juvix types to Isabelle/HOL #2689
• Adds the command juvix isabelle program.juvix which translates a given file to an Isabelle/HOL theory.
• Currently, only a single module is translated.
• By default translates types and function signatures. Translating function signatures can be disabled with the --only-types option.

Blocked by:

• Internal-to-Core translation is limited to type-declaring axioms #2763

[janmasrovira]

any ideas of how this could be tested?

Maybe we could have a parser for the subset of isabelle that we are producing. Then we would manually write the expected isabelle file and store it in the test suite, and then we would compare asts between the generated code and the parsed code. We could also compare the text if we don't wan't to write a parser, but that's a bit brittle.

[lukaszcz]

any ideas of how this could be tested?

Maybe we could have a parser for the subset of isabelle that we are producing. Then we would manually write the expected isabelle file and store it in the test suite, and then we would compare asts between the generated code and the parsed code. We could also compare the text if we don't wan't to write a parser, but that's a bit brittle.

That's a good question. I wanted to avoid both of these solutions (both require future maintenance) but I didn't have any better idea.

How do we test HTML and Markdown generation?

[jonaprieto]

How do we test HTML and Markdown generation?

For Markdown, we have tests in test/BackendMarkdown/ and smoke tests. For Html, as far as I remember, we only have smoke tests.

any ideas of how this could be tested?

Let's install Isabelle in the CI, and test with it that the generation produces valid theories.

[jonaprieto]

Wait for me, I need to test with some examples from the specs, before merging this.

[lukaszcz]

Wait for me, I need to test with some examples from the specs, before merging this.

It would be very helpful to learn what works and what still needs to be implemented/improved, but aside of obvious bugs I think any feature requests should be delegated to separate future PRs. So that we have an initial working version first, even if it's somewhat restricted in what it can handle.

[jonaprieto]

The theory's name must correspond to the file's name. Currently, it's printing the qualified name of the Juvix module.

[lukaszcz]

When is the generated file name different from the qualified named of the Juvix module? I think it's always the same.

[lukaszcz]

Can theory names in Isabelle contain dots?

[jonaprieto]

I got an error that says "Bad theory name .. with qualification" if we use dots.
However, I couldn't find any mention of this in the "Isabelle System Manual." So, they probably want the names of theories to be like regular names.

[lukaszcz]

Okay, maybe then I just replace . with e.g. __ in both file and theory names.

[jonaprieto]

That won't work either. Use the unqualified name of the module as the name of the theory.

[lukaszcz]

Okay, can do that (potentially problematic in the future when translating multiple modules).

[jonaprieto]

Indeed. But we can generate the Isabelle theories following the module's folder structure of the Juvix modules. We do this for HTML output. We can do that in the future.

[lukaszcz]

Done

[lukaszcz]

For Markdown, we have tests in test/BackendMarkdown/ and smoke tests.

The single positive markdown test is very brittle because it just compares the output to a pre-stored file. I just had to regenerate it after changing some unrelated thing in the scoper, which changed the nameId numbers, which changed the generated markdown text.