Skip to content

Commit

Permalink
Merge pull request #2113 from GaloisInc/prepare-release-v1.2
Browse files Browse the repository at this point in the history
Prepare release v1.2
  • Loading branch information
mccleeary-galois authored Sep 3, 2024
2 parents 47a7632 + d6b6062 commit 6afd8e7
Show file tree
Hide file tree
Showing 13 changed files with 133 additions and 136 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ env:
# older .so files are cached, which can have various effects
# (e.g. cabal complains it can't find a valid version of the "happy"
# tool).
CABAL_CACHE_VERSION: 1
CABAL_CACHE_VERSION: 2
SOLVER_CACHE_VERSION: 1

DISABLED_TESTS: "test0000 test_FNV_a1_rev test0010_jss_cnf_exp test0039_rust test_boilerplate test_external_abc"
Expand Down
11 changes: 8 additions & 3 deletions CHANGES.md
Original file line number Diff line number Diff line change
@@ -1,15 +1,20 @@
# next -- TBA
# Version 1.2 -- 2024-08-30

## New Features

* Add `mir_str_slice_value` and `mir_str_slice_range_value` functions, which
allow taking `&str` slices. For more information, see the documentation in the
[SAW manual](https://github.com/GaloisInc/saw-script/blob/master/doc/manual/manual.md#string-slices).

* Add `mir_mux_values` command for muxing two MIR values.

* Add support for GHC 9.8.

## Bug fixes

* The locations printed with type errors (in particular) and other diagnostics
now have a much stronger connection with reality.
* Fix bug that caused MIR to incorrectly reject overrides with multiple const slice arguments

* Error messages have been improved such that the locations printed with type errors and other diagnostics now have a much stronger connection with reality.

# Version 1.1 -- 2024-02-05

Expand Down
1 change: 1 addition & 0 deletions cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs
Original file line number Diff line number Diff line change
Expand Up @@ -671,6 +671,7 @@ parseDecls sc env input = do
let rmodule = P.Module { P.mName = P.Located P.emptyRange interactiveName
, P.mDef = P.NormalModule rdecls
, P.mInScope = mempty
, P.mDocTop = Nothing
}

-- Infer types
Expand Down
2 changes: 1 addition & 1 deletion deps/cryptol
Submodule cryptol updated 68 files
+12 −0 CHANGES.md
+1 −1 README.md
+6 −0 cryptol-remote-api/CHANGELOG.md
+9 −1 cryptol-remote-api/cryptol-eval-server/Main.hs
+5 −4 cryptol-remote-api/cryptol-remote-api.cabal
+11 −3 cryptol-remote-api/cryptol-remote-api/Main.hs
+61 −1 cryptol-remote-api/docs/Cryptol.rst
+7 −0 cryptol-remote-api/python/CHANGELOG.md
+12 −0 cryptol-remote-api/python/cryptol/commands.py
+9 −0 cryptol-remote-api/python/cryptol/connection.py
+1 −1 cryptol-remote-api/python/pyproject.toml
+150 −0 cryptol-remote-api/src/CryptolServer/CheckDocstrings.hs
+7 −0 cryptol-remote-api/src/CryptolServer/Exceptions.hs
+5 −4 cryptol-remote-api/src/CryptolServer/Sat.hs
+1 −1 cryptol.cabal
+56 −2 docs/RefMan/BasicSyntax.rst
+2 −2 docs/RefMan/conf.py
+92 −20 src/Cryptol/Eval/Reference.lhs
+2 −2 src/Cryptol/ModuleSystem/Interface.hs
+3 −3 src/Cryptol/Parser.y
+3 −0 src/Cryptol/Parser/AST.hs
+4 −2 src/Cryptol/Parser/Layout.hs
+94 −48 src/Cryptol/Parser/ParserUtils.hs
+28 −13 src/Cryptol/Parser/Unlit.hs
+124 −66 src/Cryptol/REPL/Command.hs
+10 −10 src/Cryptol/REPL/Help.hs
+19 −0 src/Cryptol/REPL/Monad.hs
+26 −10 src/Cryptol/Symbolic/SBV.hs
+20 −2 src/Cryptol/Symbolic/What4.hs
+55 −17 src/Cryptol/TypeCheck/AST.hs
+6 −9 src/Cryptol/TypeCheck/Infer.hs
+11 −4 src/Cryptol/TypeCheck/Module.hs
+1 −1 src/Cryptol/TypeCheck/ModuleInstance.hs
+8 −6 src/Cryptol/TypeCheck/Monad.hs
+15 −3 src/Cryptol/TypeCheck/SimpType.hs
+26 −0 src/Cryptol/TypeCheck/Solver/Numeric.hs
+8 −0 src/Cryptol/TypeCheck/Type.hs
+10 −3 tests/docstrings/T01.cry
+16 −1 tests/docstrings/T01.icry.stdout
+15 −9 tests/docstrings/T02.cry
+15 −1 tests/docstrings/T02.icry.stdout
+13 −0 tests/docstrings/T03.icry.stdout
+6 −1 tests/docstrings/T04.cry
+9 −1 tests/docstrings/T04.icry.stdout
+2 −0 tests/docstrings/T05.icry
+18 −0 tests/docstrings/T05.icry.stdout
+24 −0 tests/docstrings/T05.md
+23 −0 tests/docstrings/T06.cry
+2 −0 tests/docstrings/T06.icry
+10 −0 tests/docstrings/T06.icry.stdout
+1 −0 tests/docstrings/T07.cry
+2 −0 tests/docstrings/T07.icry
+14 −0 tests/docstrings/T07.icry.stdout
+7 −0 tests/docstrings/T07F.cry
+16 −0 tests/docstrings/T08.cry
+2 −0 tests/docstrings/T08.icry
+14 −0 tests/docstrings/T08.icry.stdout
+4 −0 tests/docstrings/T09.cry
+2 −0 tests/docstrings/T09.icry
+5 −0 tests/docstrings/T09.icry.stdout
+11 −0 tests/docstrings/T11.cry
+2 −0 tests/docstrings/T11.icry
+4 −0 tests/docstrings/T11.icry.stdout
+54 −0 tests/issues/issue1489/issue1489.cry
+1 −0 tests/issues/issue1489/issue1489.icry
+3 −0 tests/issues/issue1489/issue1489.icry.stdout
+163 −0 tests/regression/float_reference_eval.icry
+97 −0 tests/regression/float_reference_eval.icry.stdout
2 changes: 1 addition & 1 deletion deps/llvm-pretty
2 changes: 1 addition & 1 deletion deps/llvm-pretty-bc-parser
2 changes: 1 addition & 1 deletion saw-remote-api/CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
# Revision history for saw-remote-api

## next -- TBA
## 1.2.0 -- 2024-08-30

* Add `"str slice"` and `"str slice range"` `setup value`s, which are used to
represent MIR `str` slice references. Attempting to use these in LLVM or JVM
Expand Down
2 changes: 1 addition & 1 deletion saw-remote-api/python/CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
# Revision history for saw-client

## next -- TBA
## 1.2.0 -- 2024-08-30

* Add `str_slice()` and `str_slice_range()` functions for constructing MIR `str`
slice references. Using these functions with LLVM or JVM verification will
Expand Down
235 changes: 113 additions & 122 deletions saw-remote-api/python/poetry.lock

Large diffs are not rendered by default.

4 changes: 2 additions & 2 deletions saw-remote-api/python/pyproject.toml
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
[tool.poetry]
name = "saw-client"
version = "1.1.1.99"
version = "1.2.0.99"
readme = "README.md"
description = "SAW client for the SAW RPC server"
authors = ["Galois, Inc. <[email protected]>"]
Expand All @@ -14,7 +14,7 @@ include = [
python = "^3.8"
requests = "^2.25.1"
BitVector = "^3.4.9"
cryptol = "3.1.1" # { path = "../../deps/cryptol/cryptol-remote-api/python/", develop = true }
cryptol = "3.2.0" # { path = "../../deps/cryptol/cryptol-remote-api/python/", develop = true }
argo-client = "0.0.12"
lmdb = "^1.4.1"
cbor2 = "^5.4.6"
Expand Down
2 changes: 1 addition & 1 deletion saw-remote-api/saw-remote-api.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ cabal-version: 2.4
-- http://haskell.org/cabal/users-guide/

name: saw-remote-api
version: 1.1.0.99
version: 1.2.0.99
-- synopsis:
-- description:
-- bug-reports:
Expand Down
2 changes: 1 addition & 1 deletion saw-script.cabal
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
Cabal-version: 2.4
Name: saw-script
Version: 1.1.0.99
Version: 1.2.0.99
Author: Galois Inc.
Maintainer: [email protected]
Build-type: Custom
Expand Down

0 comments on commit 6afd8e7

Please sign in to comment.