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.

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

Support Coq 8.15, 8.16 in support libraries #1750

Merged
merged 2 commits into from
Nov 18, 2022
Merged

Support Coq 8.15, 8.16 in support libraries #1750

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
bf0c81e
Support Coq 8.15, 8.16 in support libraries
RyanGlScott Oct 10, 2022
9f028a6
Merge branch 'master' into T1601
mergify[bot] Nov 18, 2022
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
8 changes: 6 additions & 2 deletions saw-core-coq/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,10 +33,14 @@ opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-bits
```

If you run into any issue that is probably due to the version mismatch between the `ocamlc`
and the `ocaml` base system installed on your machine and it can be fixed as explained
If you run into any issue that is probably due to the version mismatch between the `ocamlc`
and the `ocaml` base system installed on your machine and it can be fixed as explained
[here](https://github.com/ocaml/opam/issues/3708).

Currently, the Coq support libraries for `saw-core-coq` requires Coq 8.13 or
later. In particular, they are known to build with Coq 8.13, 8.15, and 8.16,
but *not* 8.14 (see [this
issue](https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Code.20typechecks.20in.20Coq.208.2E13.2C.20but.20not.20in.208.2E14)).

## Building the and Using the Coq Support Libraries

Expand Down
2 changes: 1 addition & 1 deletion saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -230,7 +230,7 @@ Definition sbvToInt (n : Nat) (b : bitvector n) : Z

(* Useful notation for bools *)
Definition boolToInt (b : bool) : Z := if b then 1%Z else 0%Z.
Numeral Notation bool Z.odd boolToInt : bool_scope.
Number Notation bool Z.odd boolToInt : bool_scope.
Close Scope bool_scope. (* no, don't interpret all numbers as booleans... *)

(* This is annoying to implement, so using BITS conversion *)
Expand Down