Skip to content

SAWCore Float support #3362

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.

Sign up for GitHub

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

Open
RyanGlScott wants to merge 3 commits into
base: master
Choose a base branch
from
+5,040 −715
Open

SAWCore Float support #3362

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
b00a453
Whitespace only
RyanGlScott Aug 4, 2026
f070c4e
otherTests/saw-core-rocq: Add *.rawlog to .gitignore
RyanGlScott Aug 12, 2026
6143453
SAWCore Float support
RyanGlScott Feb 20, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 4 additions & 2 deletions .github/workflows/ci.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -611,12 +611,14 @@ jobs:
- run: opam pin add -y rocq-prover 9.0.0
- run: opam install -y rocq-core=9.1.0 rocq-stdlib=9.0.0

# Install coq-bits from source. FIXME: replace with compatible
# opam-released version when available.
# Install coq-bits and coq-flocq from source.
# FIXME: replace pinned versions with compatible opam-released versions
# when available.
- working-directory: saw-core-rocq/rocq
run: |
opam install -y coq=9.1.0 # coq-* packages include compatibility shims (e.g., coq_makefile).
opam pin -y coq-bits https://github.com/rocq-community/bits.git#f50fc3e5f1eabcb0b0b94c8d25f75e61a255c2ba
opam pin -y coq-flocq https://gitlab.inria.fr/flocq/flocq.git#27143972fc1dc96e281626d5194b5b371f05db80

# FIXME: the following steps generate Rocq libraries for the SAWCore to
# Rocq translator and builds them; if we do other Rocq tests, these steps
Expand Down
2 changes: 1 addition & 1 deletion CHANGES.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,7 @@ This release supports [version
corresponding to a source file and source line number, or (3) the unnamed
Metadata at the requested index.

* Add basic support for Cryptol `Rational` values in SAWCore.
* Add basic support for Cryptol `Rational` and `Float` values in SAWCore.

* Add support for derived Cryptol instances in SAWCore.

Expand Down
Loading
Loading