Merge reset_shift into master #20
Draft
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…re are normalisation going on
The example is taken from Asai's tutorial. Heifer cannot verify this example. Hopefully that there is no mistake in the translation of this example.
The function is found in Asai's tutorial. Heifer can verify this example, however, when we have the second reset, the verifier throw an error in verification time, saying that "domain is not disjoint".
Merge reset_shift and master This commit is massive, which is not a good thing smh. Currently, the build is falling due to some problem with the parsers. We will address these problems in the next commit.
twice into MenhirLib inside parser.mli Now we have a problem with Racketfrontend, the module does not exist during build. Why?
The fix is to add `racketfrontend` into the `libraries` stanza under `hiplib` - this dependency was not declared.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This is a massive PR.
Currently, there is no compilation error, but the build is still falling due to problems occur in
boot/menhir/dune. I am trying to resolve this issue.A summary of main changes will be added later, once the build works again.