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

Update type-check CI to include literate specs #168

Open
1 of 5 tasks
mccleeary-galois opened this issue Oct 31, 2024 · 1 comment
Open
1 of 5 tasks

Update type-check CI to include literate specs #168

mccleeary-galois opened this issue Oct 31, 2024 · 1 comment
Labels
CI good first issue Good for newcomers

Comments

@mccleeary-galois
Copy link
Contributor

mccleeary-galois commented Oct 31, 2024

Summary

Type-check CI currently does not check literate specs only .cry files.

https://github.com/GaloisInc/cryptol-specs/blob/master/scripts/load_all_cry_files.sh#L19

Note that not all .md and .tex files are literate cryptol.

Acceptance Criteria

Update CI to check literate specs as well.

Do

  • define acceptance criteria
  • add appropriate labels
  • remember to update CHANGES
  • remember to update docs appropriately
  • CI properly type checks literate specs as well
@WeeknightMVP
Copy link

Cryptol fails to load the following Markdown files, which have unlabeled code fences containing non-Cryptol:

Primitive/Asymmetric/KEM/ML_KEM/README.md
Primitive/Asymmetric/Signature/Dilithium/README.md
Primitive/Asymmetric/Signature/FALCON/1.2/README.md
Primitive/Asymmetric/Signature/SphincsPlus/README.md

Adding an info string such as ```console (or anything not starting with ```cryptol) would render them loadable (as non-modules adding no definitions) by the Cryptol REPL or Remote API.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
CI good first issue Good for newcomers
Projects
None yet
Development

No branches or pull requests

2 participants