From bf0c81ed5768f3c5b6a36ad0514a7d5abdca184e Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 10 Oct 2022 15:14:15 -0400 Subject: [PATCH] Support Coq 8.15, 8.16 in support libraries This requires a small change from `Numeral Notation` notation to `Number Notation`, the former of which was removed in Coq 8.15. The latter is only supported in Coq 8.13 or later, so I have documented this in the `saw-core-coq` `README`. Fixes #1601. --- saw-core-coq/README.md | 8 ++++++-- .../handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v | 2 +- 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/saw-core-coq/README.md b/saw-core-coq/README.md index 49338979c8..be4f53af03 100644 --- a/saw-core-coq/README.md +++ b/saw-core-coq/README.md @@ -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 diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v index a32846b4c1..9b610324ff 100644 --- a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v +++ b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreVectorsAsCoqVectors.v @@ -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 *)