Juvix to Isabelle/HOL translation

[lukaszcz]

• Closes #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:

• https://github.com/anoma/juvix/issues/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.

[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.

[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.