GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-08-16 09:20:24 +03:00
Code Issues Projects Releases Wiki Activity
2,443 Commits 64 Branches 26 Tags 81 MiB
bh-fixes
Commit Graph

2443 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
brianhuffman
007e966ea6
Merge pull request #844 from GaloisInc/issue839 
Issue839
 2020-07-28 16:54:54 -07:00
Brian Huffman
fe465e108f Update expected output for regression test issue835.icry. 2020-07-28 16:03:20 -07:00
Brian Huffman
9c415a6a97 Add regression test for all implicit instance rules in cryptol. 
This includes a set of declarations in a file to test the rules
in the context of type checking. It also includes a set of type
queries to test the rules (or absence of rules) in the context
of type inference.
 2020-07-28 15:59:39 -07:00
brianhuffman
64aa778373
Merge pull request #843 from GaloisInc/issue840 
Fix typo in error messages. Fixes #840.
 2020-07-28 15:58:11 -07:00
Brian Huffman
8470e25068 Report many more unsolvable class constraints as Unsolvable. 
Also make the explanations/error messages a bit more uniform.
Fixes #839.
 2020-07-28 15:41:08 -07:00
Brian Huffman
928ac7f7a1 Fix typo in error messages. Fixes #840. 2020-07-28 15:35:35 -07:00
brianhuffman
1a2456a3a7
Merge pull request #842 from GaloisInc/issue836 
Add docstring for 'RoundingMode'. Fixes #836.
 2020-07-28 15:33:38 -07:00
Brian Huffman
b9eb076441 Add docstring for 'RoundingMode'. Fixes #836. 2020-07-28 14:58:39 -07:00
brianhuffman
cf57a0ffd2
Merge pull request #841 from GaloisInc/issue835 
Issue835
 2020-07-28 14:57:22 -07:00
Brian Huffman
e48e9f8302 Add regression test for issue #835. 2020-07-28 13:50:16 -07:00
Brian Huffman
9a5b04a98c Place parens appropriately when pretty printing types. 
Fixes #835.
 2020-07-28 13:38:56 -07:00
Aaron Tomb
5100132e4c
Tweak a few things for 2.9.0 (#833) 
* Fix Dockerfile

* Include version number in CHANGES.md

* Update copyright dates

* Don't include cryptol-specs in release archives

* Remove duplicate copy of Programming Cryptol
 2020-07-28 08:41:27 -07:00
Jared Weakly
755d4d2de3
Enable docker builds for releases and nightlies (#834) 
* Enable docker builds in nightly and release
* Fix doc builds
 2020-07-28 08:40:34 -07:00
Jared Weakly
7c082b475c
Allow release branches to actually release (#832) 
Fix release check
 2020-07-27 10:05:28 -07:00
robdockins
c4b083bcbb
Merge pull request #793 from GaloisInc/parameterized-file-reader 
Parameterize module system over filesystem access
 2020-07-27 09:53:29 -07:00
Jared Weakly
12cdace222
Merge pull request #821 from GaloisInc/actions/improve-release-ux 
Improve release ux
 2020-07-24 16:41:55 -07:00
Jared Weakly
7e5e1ca439 explicitly build cryptol-html target in addition to cryptol 2020-07-24 15:03:38 -07:00
David Thrane Christiansen
d952f168e6 Parameterize module system over filesystem access 
Adds the ability for clients of Cryptol-the-library to provide their
own means of accessing disk, as a sort of lightweight VFS. This will
be used for caching multiple concurrent states in SAW.
 2020-07-24 14:14:37 -07:00
Jared Weakly
19f643a3ce add working retry 2020-07-24 14:12:41 -07:00
Jared Weakly
66f7aa2165 Deduplicate release checking logic 2020-07-24 14:12:41 -07:00
Jared Weakly
4832160fd9 Add release versioning for cryptol 2020-07-24 14:12:41 -07:00
Jared Weakly
4c9ee03b59 Manually invalidate cache for dist-newstyle 2020-07-24 14:12:41 -07:00
Jared Weakly
2b12784e63 typo: releases -> release 2020-07-24 14:12:41 -07:00
Jared Weakly
5f36effaee Ignore harmless errors if strip fails 2020-07-24 14:12:41 -07:00
Jared Weakly
ad76a58e08 fix cycle in yaml 2020-07-24 14:12:41 -07:00
Jared Weakly
b1b380a087 Try workaround for testing release-drafter in CI 2020-07-24 14:12:41 -07:00
Jared Weakly
97561c4613 Don't build docker image nightly yet 2020-07-24 14:12:41 -07:00
Jared Weakly
4f08953a4e Run release process on branch instead of tag 2020-07-24 14:12:41 -07:00
Jared Weakly
21be891dad Draft release using cabal file's version 2020-07-24 14:12:41 -07:00
robdockins
e2cf7d95ad
Merge pull request #830 from GaloisInc/hackage-what4 
Remove What4 submodule and depend on hackage-relased What4 instead
 2020-07-24 10:20:43 -07:00
Rob Dockins
98ee00742f Remove What4 submodule and depend on hackage-relased What4 instead. 2020-07-21 23:21:21 -07:00
Iavor Diatchki
df7d9ba906 Add a test case for #805. 
Fixes #805
 2020-07-20 17:27:16 -07:00
Iavor S. Diatchki
5d47491779
Merge pull request #822 from GaloisInc/def-eqns 
Add support for emitting definitional equations during symbolic execution
 2020-07-17 16:59:42 -07:00
Iavor Diatchki
444b8bba0d Factor out common stuff between online and offline provers, and name things 2020-07-17 12:06:07 -07:00
Iavor Diatchki
431f95392e Cleanup and renaming, but should be no much behavior changes 
The main behavior change is that we try to be more strict in the
pair keeping track of the definitions
 2020-07-17 10:13:43 -07:00
Iavor Diatchki
c654d54a6a Some progress toward collecting equations. 
This is completely untested, and some of the stuff to do with thunking
is pretty subtle, so I am not sure I got it right.

Also, I haven't gotten around to factoring the common stuff in Symbolic/What4
 2020-07-16 17:21:02 -07:00
Iavor Diatchki
c7f2a34e6b Add support for emitting definitional equations during symbolic execution. 
We use this in the definition of `fpToRational`.  It doesn't seem like
Z3 can do much with these at the moment, but maybe in the future.
 2020-07-16 14:35:21 -07:00
Iavor Diatchki
2daf5db2c1 Add a custom data structure that cobines renamer warnings 
Fixes #824
 2020-07-16 14:27:38 -07:00
Iavor Diatchki
1c34b8eb9b Add fpToRational fpFromRational and fpIsFinite. 
These are useful for switching between rationals and floats.
This also cleans up the implementation a bit, removing some duplicated
code.

NOTE: I am not sure if the translation from `float` to `rational`
is quite right in the what-4 backend, but I can't think of a better
way to do it at the moment.
 2020-07-15 17:50:15 -07:00
Iavor Diatchki
a25924df10 Add defaulting for FLiteral and update CHANGES 
Fixes #820
 2020-07-15 11:55:29 -07:00
Iavor Diatchki
eed0bdeafa Adjust comment to match declared type 2020-07-14 15:36:56 -07:00
Iavor Diatchki
39acf61ee5 Update documentation with info about floats + fractional literals 2020-07-14 15:36:37 -07:00
robdockins
bf2258b5d8
Merge pull request #819 from GaloisInc/test-updates 
Test updates
 2020-07-14 12:45:46 -07:00
Rob Dockins
c2c1ad1231 Add regression tests for the ignore-safety option 2020-07-14 12:14:36 -07:00
Iavor Diatchki
42b2ac6b45 Add parsing for binary and octal fractional literals. 
I doubt these are super common but we add them for completeness,
and because with the floats we can print in those bases
 2020-07-14 11:31:59 -07:00
Rob Dockins
bc0545bd62 Add the Eq->Cmp superclass relationship to the regression test. 2020-07-14 11:31:50 -07:00
robdockins
173a04fc01
Merge pull request #817 from GaloisInc/issue802 
Suppress the `Must be at least` line of defaulting error
 2020-07-14 11:27:26 -07:00
Aaron Tomb
2f4684c8af
Build system and documentation cleanup (#816) 
* Remove `Makefile`
* Remove Travis and AppVeyor configurations
* Improve portability of the `cry` script
* Fix Docker builds
* Update documentation to remove references to `make`
* Update copyright dates
* Fix omitted section of CONTRIBUTING.md
* Update Z3 installation instructions

Fixes #570, #603, #790, #807.
 2020-07-14 10:58:38 -07:00
Iavor Diatchki
6e412ed32e A hack to always print .0 for non base 10 numbers. 
This helps with copy-pasting values, as non base 10 literals
are not overloaded.
 2020-07-14 10:47:30 -07:00
Rob Dockins
bccc098a2b Suppress the Must be at least line of defaulting error 
messages when the calculated bound is 0.
 2020-07-14 10:32:57 -07:00