Commit Graph

3999 Commits

Author SHA1 Message Date
Bretton
57aee9e7f9 Update ffi-runtime-errors test output 2023-08-21 19:44:40 -07:00
Bretton
9a8f870664 FFINotSupported error message formatting 2023-08-21 19:43:24 -07:00
Bretton
fc9e6bdcdc Add fallback for foreign in reference evaluator 2023-08-21 19:41:57 -07:00
Bretton
50c0cb8a66 Fall back to cryptol version of foreign functions 2023-08-21 19:26:10 -07:00
Bretton
7f7ec412ea Define foreignLibPath when FFI disabled
Fixes build error when FFI is disabled.
2023-08-21 18:49:33 -07:00
Bretton
58a3b06796 Allow cryptol implementation of foreign functions 2023-08-21 10:46:49 -07:00
Bretton
cd5d006277
Merge pull request #1559 from GaloisInc/T1455
Make names in scope in functors accessible when their instantiations are loaded at the REPL
2023-08-10 17:06:09 -07:00
Bretton
fbfad1fd0c Add test for #1562 2023-08-10 15:39:24 -07:00
Bretton
bcb60f2ef4 Add missing interface type synonyms to instMap 2023-08-10 15:29:12 -07:00
Iavor Diatchki
f8ab523e4c Remove unused interface field. 2023-08-09 16:42:36 -07:00
Iavor Diatchki
407d78c9e3 Rename things, and add comments. 2023-08-09 16:30:32 -07:00
Iavor Diatchki
064f391a04 Update CHANGES 2023-08-09 16:30:11 -07:00
Bretton
edff7d3088 Fix test output for issues/issue1455_3 on windows 2023-08-08 18:34:13 -07:00
Bretton
fbb2e37bdd Add tests for #1561 2023-08-08 17:45:12 -07:00
Bretton
bff4add099 Fix tests/issues/issue1455/Inst1.cry 2023-08-08 17:42:35 -07:00
Bretton
999ba7b5b3 Add tests for #1455 2023-08-08 17:07:46 -07:00
Bretton
5cd34d0afb Qualify FromFunctorInst OrigNames by interface 2023-08-08 15:53:24 -07:00
Bretton
09fba48ac0 Keep FromModParam sig name in namingEnvFromNames 2023-08-07 15:26:56 -07:00
Bretton
44dd5908e4 Remove mod params from inScope in _ instantiation 2023-08-04 11:21:40 -07:00
Bretton
6a0121cb04 Add type synonym for type params in instantiations 2023-08-03 17:03:35 -07:00
Bretton
d6791fd1c5 Rename confusing arg in checkParamValue 2023-08-02 15:46:13 -07:00
Bretton
e9b3b5f6a6 Make fresh name for value params in instantiations 2023-08-02 15:20:08 -07:00
Ryan Scott
6acbd46aea
RefMan: document that the FFI expects pure functions (#1558)
This is a disclaimer that while you _can_ use impure functions in the Cryptol
FFI, we make no guarantees about the precise behavior of the side effects that
they functions may perform.

Fixes #1554.
2023-07-31 07:26:17 -04:00
Bretton
632adf480a Add comment in doFunctorInst explaining inScope 2023-07-28 18:46:26 -07:00
Bretton
9b3ab47319 Add functor in-scope info to its instantiations 2023-07-28 18:01:51 -07:00
dependabot[bot]
9de24f5063
Bump certifi from 2022.12.7 to 2023.7.22 in /cryptol-remote-api/python (#1555)
Bumps [certifi](https://github.com/certifi/python-certifi) from 2022.12.7 to 2023.7.22.
- [Commits](https://github.com/certifi/python-certifi/compare/2022.12.07...2023.07.22)

---
updated-dependencies:
- dependency-name: certifi
  dependency-type: indirect
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
2023-07-26 10:26:53 -04:00
Ryan Scott
383a5974e2
Merge pull request #1550 from GaloisInc/T1548-part-two
Build against `sbv-10.2`
2023-07-13 12:46:17 -04:00
Ryan Scott
a045188b18 README: Fix typo 2023-07-13 11:37:26 -04:00
Ryan Scott
f2bf0ec8fa CI: Set UTF-8 in cryptol-remote-api's portable build 2023-07-13 08:51:08 -04:00
Ryan Scott
77a52e3bb6 CI: Prefer Use 9.2.8 (not 8.10.7) for building Docker images
There are two motivations for doing so:

* `sbv-10.0` and later no longer build against GHC 8.10 (see
  https://github.com/LeventErkok/sbv/issues/655), but we want to use a new `sbv`
  version to come to a resolution to #1548. As such, we need a newer GHC.
* `ghcup` now recommends GHC 9.2.8 for most usage, so it's time we switched
  anyway.
2023-07-12 10:24:49 -04:00
Ryan Scott
71a8f86fb4 CI: Use GHC 9.2.8, 9.4.5 2023-07-12 07:51:28 -04:00
Ryan Scott
9ea9005320 Allow building with sbv-10.2 2023-07-12 07:31:56 -04:00
Ryan Scott
cee5b835b1
Merge pull request #1549 from GaloisInc/T1548
CI: Bump what4-solvers snapshot to 20230711
2023-07-11 14:14:48 -04:00
Ryan Scott
5a85fae631 CI: Leave some breadcrumbs about SOLVER_PKG_VERSION and BIN_ZIP_FILE
This will make it easier for future devs to remember what places need to be
updated.
2023-07-11 13:32:49 -04:00
Ryan Scott
693f82f1b1 CI: Bump what4-solvers snapshot to 20230711
This includes the following changes:

* The bindist URLs now include the OS architecture, I have tweaked the parts of
  CI that downloads bindists accordingly.
* This snapshot includes `cvc5-1.0.5`, which has fixed a bug that was
  responsible for #1548. As such, this fixes #1548.
2023-07-11 12:53:15 -04:00
Matthew Yacavone
2064a38b8c
Merge pull request #1547 from GaloisInc/version-python-cmd
Add `version` command to cryptol-remote-api
2023-07-10 15:49:01 -04:00
Matthew Yacavone
9e86c0fa25 Bump cryptol-remote-api versions to 3.0.1.99 development version 2023-07-10 13:45:33 -04:00
Matthew Yacavone
75d00d9dfc Bump cryptol-remote-api versions to 3.0.1 2023-07-10 13:45:29 -04:00
Matthew Yacavone
a5366b97ff use when function in Version.hs 2023-07-10 13:25:36 -04:00
Matthew Yacavone
9831dc8ddd update docs with version command 2023-07-10 13:25:36 -04:00
Matthew Yacavone
d914b803ce update CHANGELOG for Python API 2023-07-10 13:25:32 -04:00
Matthew Yacavone
39759bba06 include cryptol-remote-api version in version command 2023-07-10 13:25:02 -04:00
Ryan Scott
2919e6bbc9
Merge pull request #1543 from GaloisInc/T1542
Modernize the `README` slightly
2023-07-06 15:52:58 -04:00
Matthew Yacavone
1f7cdb83c3 add version command to cryptol-remote-api 2023-07-06 15:41:42 -04:00
Ryan Scott
dd0151540e cryptol-remote-api: Don't hardcode version number in project description
It's easy to forget to update this. In addition, the version number is
specified elsewhere in the pyproject.toml file, so putting the version number
in the description in redundant.
2023-07-06 14:54:57 -04:00
Matthew Yacavone
68e48dd4dc
Merge pull request #1541 from GaloisInc/sanitize-strs-quoting
Sanitize strings in `to_cryptol_str` in quoting.py
2023-07-06 13:58:00 -04:00
Matthew Yacavone
93b3d79f3c fixed BV and 1-tuple edge cases in to_cryptol_str 2023-07-06 13:06:58 -04:00
Matthew Yacavone
b2b5e9b4f4 add eval, latin-1 codec tests to test_quoting 2023-07-06 10:22:22 -04:00
Matthew Yacavone
e876142fdf encode strings as lists of bytes using latin-1 in to_cryptol_str 2023-07-06 10:13:39 -04:00
Ryan Scott
593f6b002c README: Acknowledge some additional Cryptol contributors
Mention Bretton Chen, Henry Blanchette, and Matthew Yacavone, all of whom have
made significant contributions. Also use Hazel Weakly's current name.
2023-07-06 08:29:38 -04:00