GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-11-10 02:09:32 +03:00
Code Issues Projects Releases Wiki Activity
4,230 Commits 66 Branches 28 Tags 85 MiB
4ca062966e
Commit Graph

4230 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Eric Mertens
4ca062966e
Initial implementation of :check-docstrings (#1682) 
* Update all commands to track their results

* Implement REPL :check-docstrings command

This command checks that all of the unlabeled and "repl" labeled
codeblocks in docstrings can successfully evaluate as REPL commands.

Cryptol will now indicate exit failure if any of REPL commands fail,
making it possible to use in automated testing.

:check-docstrings internal implementation is set up to track results
of subcommands in support for integration into a remote server API
endpoint.

* Implement :focus

* Add some :check-docstring test cases

* Update changelog

* Update CrashCourse.tex now that more commands are checked

* Require repl and convert \r\n to \n in lexer
 2024-07-18 15:44:16 -07:00
mccleeary-galois
f5fa503b18
Merge pull request #1701 from GaloisInc/issue#1675 
Close Issue #1675
 2024-07-10 15:06:10 -06:00
Ryan
dd112501ca Remove unnecessary line from issue1675 test. 2024-07-10 15:02:15 -06:00
Ryan
39b0682fbb Clean up panic error message in ec_mult 2024-07-10 13:30:17 -06:00
Ryan
873fa9cd67 Remove bigNatMod and replace with bigNatRem, and add same fix to negate as well 2024-07-10 12:31:43 -06:00
Ryan
e1774d45c1 Mod y variable by p in ec_sub 
It appears that a modulus was not happening in ec_sub that was causing the odd issue noted in #1675. This commit adds that modulus and fixes it.
 2024-07-10 11:26:37 -06:00
Ryan
84194fc187 Issue#1675, add failing test for ec_mult as y should be 0 rather than 13. 2024-07-10 10:13:11 -06:00
dependabot[bot]
e54979212b
Bump certifi from 2024.2.2 to 2024.7.4 in /cryptol-remote-api/python (#1700) 
Bumps [certifi](https://github.com/certifi/python-certifi) from 2024.2.2 to 2024.7.4.
- [Commits](https://github.com/certifi/python-certifi/compare/2024.02.02...2024.07.04)

---
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>
 2024-07-08 08:37:22 -04:00
Ryan Scott
97e972b025
Merge pull request #1695 from GaloisInc/issue1593-issue1693 
Abort early after type-checking malformed constraint guards
 2024-07-03 12:41:23 -04:00
Iavor S. Diatchki
07bb442d7e
Merge pull request #1698 from GaloisInc/issue_1691_2 
Make fixes for 1691 work with more nested modules.
 2024-07-03 09:27:22 -07:00
Iavor Diatchki
d0a98a545b Make fixes for 1691 work with more nested modules. 2024-07-03 08:57:52 -07:00
Ryan Scott
6e417aa3d1 Abort early after type-checking malformed constraint guards 
Checking ill-typed constraint guards for exhaustivity can cause Cryptol to
panic. If we detect any type errors after type-checking the guards, we now
abort early and report any recorded errors instead of proceeding to check
exhaustivity.

Fixes #1593. Fixes #1693.
 2024-07-02 07:16:05 -04:00
Ryan Scott
a483c1eddd Typofixes: s/Unexpeceted/Unexpected/g 2024-07-02 07:15:43 -04:00
Iavor S. Diatchki
623ea9bef5
Merge pull request #1692 from GaloisInc/issue_1691 
Fixes #1691 (and removes partial match warning)
 2024-07-01 19:30:10 -07:00
Iavor Diatchki
128411e605 Merge branch 'master' into issue_1691 
# Conflicts:
#	CHANGES.md
 2024-07-01 09:57:15 -07:00
Iavor Diatchki
efa9dd1742 Fix test for Windows. 2024-07-01 09:55:04 -07:00
Iavor S. Diatchki
41dceb0431
Update src/Cryptol/ModuleSystem/Renamer/ImplicitImports.hs 
Co-authored-by: Ryan Scott <rscott@galois.com>
 2024-07-01 09:35:25 -07:00
Iavor S. Diatchki
bbd08f4efd
Update CHANGES.md 
Co-authored-by: Ryan Scott <rscott@galois.com>
 2024-07-01 09:34:56 -07:00
Ryan Scott
fbbbb8f56f
Check for syntactically invalid constraint guards in the parser (#1686) 
Numeric constraint guards have very particular syntactic requirements:

* They must always be used in top-level definitions.
* Their definitions must always be accompanied by a top-level type signature.

Previously, we checked these requirements in a combination of places in the
parser and the typechecker. The checks in the typechecker weren't very
thorough, however, and they failed to catch local definitions without type
signatures that use constraint guards, as seen in #1685.

This patch moves all of these syntactic checks to the parser (in
`Cryptol.Parser.ExpandPropGuards`). We now recurse into expressions to check
for local definition that use constraint guards and error if we encounter one.
This ensures that by the time we reach the typechecker, all constraint guard
expressions are at least syntactically valid.

Fixes #1685.
 2024-07-01 07:13:36 -04:00
Ryan Scott
11e037a720
Merge pull request #1626 from GaloisInc/T1623 
`cryptol-remote-api`: Check for valid evaluation contexts
 2024-07-01 03:16:59 -07:00
Iavor Diatchki
e55470c90b Update CHANGES 2024-06-28 04:51:16 -07:00
Iavor Diatchki
84648390b7 Add a test 2024-06-28 04:39:19 -07:00
Iavor Diatchki
e98f4d6e28 Only add implicit imports for non-anonymous modules 2024-06-28 04:39:05 -07:00
Iavor Diatchki
2c6ac78f87 Fixes #1691 (and removes partial match warning) 2024-06-28 02:01:58 -07:00
Marcella Hastings
0ab12fa1cc
Merge pull request #1684 from GaloisInc/add-ubuntu-dev-setup 
Update dev-setup script to support Ubuntu 20.04 and 22.04
 2024-06-18 08:01:02 -04:00
dependabot[bot]
45103ad8b9
Bump urllib3 from 2.2.1 to 2.2.2 in /cryptol-remote-api/python (#1688) 
Bumps [urllib3](https://github.com/urllib3/urllib3) from 2.2.1 to 2.2.2.
- [Release notes](https://github.com/urllib3/urllib3/releases)
- [Changelog](https://github.com/urllib3/urllib3/blob/main/CHANGES.rst)
- [Commits](https://github.com/urllib3/urllib3/compare/2.2.1...2.2.2)

---
updated-dependencies:
- dependency-name: urllib3
  dependency-type: direct:production
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2024-06-18 06:23:55 -04:00
Marcella Hastings
36a6f576f6 dev-script: fix env variable handling #1673 
- change dockerfiles to hardcode environment variables instead of trying
  to source them from the script
- Fix a typo in setting LANG
 2024-06-13 15:14:09 -04:00
Marcella Hastings
05392cf94d dev-setup: small script improvements #1673 
- handle non-debian linux platforms correctly
- reduce automatic destruction of user language settings
- improve documentation
- fix dockerfiles to actually run the script
 2024-06-13 14:07:57 -04:00
Marcella Hastings
1952c8b4ff dev-setup: prettify script #1673 
- clarifies errors that should be unreachable
- reduces duplication with a function to check version
 2024-06-11 09:38:37 -04:00
Marcella Hastings
918335bf93 dev-setup: add support for ubuntu-22.04 #1673 2024-06-11 09:38:37 -04:00
Marcella Hastings
73a6e683d7 dev-setup: add support for ubuntu 20.04 #1673 2024-06-11 09:38:27 -04:00
Marcella Hastings
cb9b2b28f1 dev-setup: add minimal docker for ubuntu 20 #1673 2024-06-11 09:38:27 -04:00
Marcella Hastings
8df304dc76 dev-setup: move script to dev/ dir #1673 2024-06-11 09:38:19 -04:00
Marcella Hastings
94c8db0a7d
Merge pull request #1674 from GaloisInc/add-macos-dev-setup 
add dev_setup script for macOS 14
 2024-06-05 09:05:11 -04:00
Marcella Hastings
4a7f0a8513 use specific ghc/cabal versions in dev setup #1673 2024-06-05 08:36:52 -04:00
Marcella Hastings
e03e7be18f simplify ghc install in dev script #1673 
- stop running script from the internet; start using nice commands
- ghc install now depends on brew, so rewrote the brew path stuff
- fixes small quoting issues and bashisms
 2024-06-04 07:17:55 -04:00
Eric Mertens
20d88b8401
Merge pull request #1664 from GaloisInc/remember-docstrings 
Avoid discarding any docstring comments
 2024-06-03 13:53:54 -07:00
Marcella Hastings
0380a45d89 consolidate funcs, improve errors in setup script 2024-06-03 16:22:05 -04:00
Eric Mertens
1009680664 Remove docstrings from 'include' 2024-06-03 10:09:40 -07:00
Eric Mertens
823ed91fc7 Update docs.cry test to show preserved doctests 2024-06-03 10:09:40 -07:00
Eric Mertens
ec94131db5 Avoid discarding any docstring comments 
* include, import, and type constraint docstrings are now preserved
* parameter and private block docstrings are not supported
 2024-06-03 10:09:40 -07:00
Marcella Hastings
e25afff519 Fix distro and version checks in dev script #1673 
- Fixes some control flow and methods for checking what distribution
  we're on
- Adds a version check for CVC4 and 5
- Modifies and documents behavior for env.sh file
- Removes some bashisms and accidental use of fancy names
 2024-06-03 11:21:14 -04:00
Iavor S. Diatchki
c6b4209816
Merge pull request #1678 from GaloisInc/issue_1490 
Fixes #1490
 2024-06-02 19:30:02 +03:00
Iavor Diatchki
d6eed17be5 More test fixes 2024-06-02 07:13:27 -07:00
Iavor Diatchki
c77db36a25 Update mingw test 2024-06-02 04:20:31 -07:00
Iavor Diatchki
a9f962a5e7 Fix darwin test 2024-06-02 04:16:37 -07:00
Iavor Diatchki
4f2cf7d5fa Use Integer in head and last. 
This is a bit of an overkill, as clearly 0 doesn't need it,
but it ensures maximum compatibility with the old behavior.
 2024-06-02 00:04:53 -07:00
Iavor S. Diatchki
332e50cc10
Merge pull request #1362 from GaloisInc/T1353 
Always embed `git` commit into `--version` output
 2024-06-01 03:08:18 -07:00
Iavor Diatchki
d599934038 Fix tests 2024-06-01 03:04:15 -07:00
Iavor S. Diatchki
9a62f7cf6e
Merge pull request #1677 from GaloisInc/issue_1672 
Fixes #1672
 2024-06-01 01:59:14 -07:00