GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-10-05 18:08:04 +03:00
Code Issues Projects Releases Wiki Activity
4,290 Commits 65 Branches 28 Tags 85 MiB
master
Commit Graph

273 Commits

Author SHA1 Message Date
Ryan
75a61ec3d3 Update Generate Test Vector Example 
Use different size output to reiterate that the output is first in the results of :dumptests.

Some minor rewording and wordsmithing.
 2024-10-02 10:02:00 -06:00
Ryan
ce8e3f1b20 Change example in Generate test vector section to not reference cryptol specs. 
Keep example as a polymporphic function using multiple inputs and a non Bit output to show that it can handle that case now.

Also fix up some minor typos and clarify a few sentences.
 2024-10-01 14:07:29 -06:00
Ryan
7f8780e57f Close #611: Add new section to the High Assurance chapter of the Programming Cryptol book for generating test vectors using :dumptests. 
An example is also given using SHA2 256.
 2024-10-01 11:25:35 -06:00
Marcella Hastings
d6c1f0f979 docs: improve docs about docs 
- updates contributing file with a brief overview of kinds of
  user-facing documentation
- minor updates to book-building CI documentation
 2024-09-20 13:04:59 -04:00
Marcella Hastings
84f1049d03 update cryptol book pdf with recent changes 2024-09-19 14:05:35 -04:00
Marcella Hastings
b7363dd99f Update type of take in book 2024-09-10 10:06:09 -04:00
Ryan
afb8730af4 Cryptol 3.2 Release: Update Cabal version numbers. 2024-08-20 09:43:15 -06:00
Eric Mertens
009907ed91
Improve :check-docstrings (#1706) 
* Document docstring comments in reference manual
* Handle more expected cases of prefix stripping in docstring comments
* Catch REPL exceptions when checking docstrings
 2024-07-23 09:43:43 -07:00
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
David Holland
facc682fe8
Fix some typos I noticed in the Programming Cryptol book. (#1631) 
- p-1 bits in an IEEE float refers to the significand, not the
  mantissa, at least according to the latest preferred terminology,
  which aims to keep the word "mantissa" for the full mantissa
  including the units bit;
- reciprocal rather than reciprocol;
- the example in 1.23 had the wrong module declarations; also insert a
  separator word between the verbatim blocks so they can be told
  apart.
 2024-02-23 08:16:07 -05:00
Ryan Scott
01d8c1d32f Repair ProgrammingCryptol test 2024-02-01 18:55:56 -05:00
Ryan Scott
56cf1a373d Repair ProgrammingCryptol test 2024-02-01 18:22:34 -05:00
Ryan Scott
76f9c3eac3 RefMan: Regenerate HTML 2024-02-01 16:55:00 -05:00
Ryan Scott
75958c1ef2 RefMan: Fix formatting error 2024-02-01 16:54:09 -05:00
Ryan Scott
8732b32246 Add Option and Result types to the Cryptol prelude 
These are useful enough that it is worth defining them in the standard library.
 2024-02-01 16:53:25 -05:00
Ryan Scott
2f5bbd97bd Clarify "Known Enum Type" restriction in RefMan 2024-02-01 16:24:01 -05:00
Ryan Scott
c8e4615307
Apply suggestions from code review 2024-02-01 16:21:18 -05:00
Iavor Diatchki
684a85ed18 Tweak error messages 2024-01-31 10:36:13 -08:00
Ryan Scott
d965cb44ae Emit an error for non-exhaustive case expressions 
Fixes #1608.
 2024-01-28 17:15:55 -05:00
Ryan Scott
17b1e259d1 RefMan: Say "enums", not "enumerations", to avoid ambiguous terminology 2024-01-26 10:54:15 -05:00
Ryan Scott
eb4a4cea4c Document no-overlapping-patterns restriction 2024-01-26 10:40:20 -05:00
Iavor Diatchki
e975355d3f Document enum declarations 2024-01-22 15:41:00 -08:00
Bretton
0e068c92b4 Reword RefMan section on FFI cryptol fallback 2023-08-22 14:02:17 -07:00
Bretton
66bdbf5084 Document FFI fallback implementation in RefMan 2023-08-22 13:54:41 -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
Kevin Quick
b1910c8775
Fix some syntax errors in the Modules documentation. 2023-06-27 14:13:20 -07:00
Kevin Quick
cb825cf4a6
Docs redirect reset to standard Galois cryptol location. 2023-06-21 17:11:44 -07:00
Kevin Quick
1318643cc0
Enable Github CI build of documentation for all tags and PRs. 2023-06-20 22:41:10 -07:00
Iavor Diatchki
77fd64f8ec Merge branch 'master' into functors-merge 
# Conflicts:
#	docs/RefMan/_build/doctrees/BasicSyntax.doctree
#	docs/RefMan/_build/doctrees/BasicTypes.doctree
#	docs/RefMan/_build/doctrees/Expressions.doctree
#	docs/RefMan/_build/doctrees/FFI.doctree
#	docs/RefMan/_build/doctrees/Modules.doctree
#	docs/RefMan/_build/doctrees/OverloadedOperations.doctree
#	docs/RefMan/_build/doctrees/RefMan.doctree
#	docs/RefMan/_build/doctrees/TypeDeclarations.doctree
#	docs/RefMan/_build/doctrees/environment.pickle
#	docs/RefMan/_build/html/.buildinfo
#	docs/RefMan/_build/html/BasicSyntax.html
#	docs/RefMan/_build/html/BasicTypes.html
#	docs/RefMan/_build/html/Expressions.html
#	docs/RefMan/_build/html/FFI.html
#	docs/RefMan/_build/html/Modules.html
#	docs/RefMan/_build/html/OverloadedOperations.html
#	docs/RefMan/_build/html/RefMan.html
#	docs/RefMan/_build/html/TypeDeclarations.html
#	docs/RefMan/_build/html/_static/basic.css
#	docs/RefMan/_build/html/_static/css/badge_only.css
#	docs/RefMan/_build/html/_static/css/theme.css
#	docs/RefMan/_build/html/_static/doctools.js
#	docs/RefMan/_build/html/_static/jquery.js
#	docs/RefMan/_build/html/_static/js/theme.js
#	docs/RefMan/_build/html/_static/searchtools.js
#	docs/RefMan/_build/html/_static/underscore.js
#	docs/RefMan/_build/html/genindex.html
#	docs/RefMan/_build/html/search.html
#	docs/RefMan/_build/html/searchindex.js
 2023-05-25 11:38:40 -07:00
Iavor Diatchki
08783625c1 Document the classes that inhabit the various overloading classes. 2023-05-23 11:23:36 -07:00
Ian Sweet
6ee9220a53 cryptol module docs: tightened some writing, fixed some typos, and introduced the term 'functor' as it was used without definition. 2023-03-23 11:05:11 -04:00
Iavor Diatchki
7f793d786b Update the reference manual to document instantiating with _ 2022-12-21 16:39:27 -08:00
Iavor Diatchki
fa8fa4617e Merge remote-tracking branch 'origin/master' into functors-merge 2022-11-21 16:33:27 -08:00
Iavor Diatchki
11c0efe1d8 Fixup line numbers in docs and update CHANGES 2022-11-21 10:24:56 -08:00
Iavor Diatchki
2d359532f4 Update the documentation 2022-10-25 15:18:58 -07:00
Iavor Diatchki
441e163856 Merge branch 'master' into functors-merge 
# Conflicts:
#	docs/RefMan/_build/doctrees/BasicSyntax.doctree
#	docs/RefMan/_build/doctrees/BasicTypes.doctree
#	docs/RefMan/_build/doctrees/Expressions.doctree
#	docs/RefMan/_build/doctrees/FFI.doctree
#	docs/RefMan/_build/doctrees/Modules.doctree
#	docs/RefMan/_build/doctrees/OverloadedOperations.doctree
#	docs/RefMan/_build/doctrees/RefMan.doctree
#	docs/RefMan/_build/doctrees/TypeDeclarations.doctree
#	docs/RefMan/_build/doctrees/environment.pickle
#	docs/RefMan/_build/html/.buildinfo
#	docs/RefMan/_build/html/BasicSyntax.html
#	docs/RefMan/_build/html/BasicTypes.html
#	docs/RefMan/_build/html/Expressions.html
#	docs/RefMan/_build/html/FFI.html
#	docs/RefMan/_build/html/Modules.html
#	docs/RefMan/_build/html/OverloadedOperations.html
#	docs/RefMan/_build/html/RefMan.html
#	docs/RefMan/_build/html/TypeDeclarations.html
#	docs/RefMan/_build/html/_static/doctools.js
#	docs/RefMan/_build/html/_static/fonts/Lato-Bold.ttf
#	docs/RefMan/_build/html/_static/fonts/Lato-Regular.ttf
#	docs/RefMan/_build/html/_static/js/modernizr.min.js
#	docs/RefMan/_build/html/_static/searchtools.js
#	docs/RefMan/_build/html/searchindex.js
#	src/Cryptol/ModuleSystem.hs
#	src/Cryptol/ModuleSystem/Base.hs
#	src/Cryptol/ModuleSystem/InstantiateModule.hs
#	src/Cryptol/Parser/AST.hs
#	src/Cryptol/Parser/ParserUtils.hs
#	src/Cryptol/REPL/Command.hs
#	src/Cryptol/Transform/AddModParams.hs
#	src/Cryptol/Transform/Specialize.hs
#	src/Cryptol/TypeCheck/Infer.hs
#	src/Cryptol/TypeCheck/InferTypes.hs
#	src/Cryptol/Utils/Ident.hs
 2022-09-27 11:43:16 +03:00
Ryan Scott
27ac8d9717 Support FFI on Windows 
This patch:

* Adds the appropriate conditional logic to use the `Win32` library to
  dynamically load shared libraries on Windows.
* Tweaks some FFI-related test cases to make them work portably on Windows. I
  have left comments describing each of the non-obvious tweaks that I had to
  make.
* Updates the reference manual accordingly.

Fixes #1394.
 2022-09-24 11:21:03 -04:00
Iavor Diatchki
e7a3f87858 Update FFI Section of Reference Manual to describe Integer/Rational/Z 2022-09-22 18:30:03 +03:00
Iavor Diatchki
5a4a3967fc Merge remote-tracking branch 'origin/master' into ffi-generate-headers 
# Conflicts:
#	docs/RefMan/_build/doctrees/FFI.doctree
#	docs/RefMan/_build/doctrees/environment.pickle
#	docs/RefMan/_build/html/FFI.html
#	docs/RefMan/_build/html/searchindex.js
 2022-09-14 17:18:30 +03:00
Iavor S. Diatchki
51b765efd8
Merge pull request #1431 from GaloisInc/ffi-slides 
Add FFI presentation slides
 2022-09-14 16:40:17 +03:00
Bretton
387a15e14c Add FFI presentation slides 2022-09-08 18:28:30 -07:00
Bretton
986ec22ac7 gen header: Update refman 2022-09-08 17:39:18 -07:00
Iavor Diatchki
b86825b7c4 Update text in the "Numeric Constraint Guards" section 2022-09-03 11:56:57 +03:00
Henry Blanchette
28f34df25e can be -> are 2022-08-30 08:55:46 -07:00
Henry Blanchette
1cfad8affc updated to master 2022-08-22 13:34:27 -07:00
Bretton
2f4b821eab FFI: Add docs for nested sequences 2022-08-17 14:50:26 -07:00
Henry Blanchette
c33c3fd1c4 updated docs [ci skip] 2022-08-13 14:22:26 -07:00
Henry Blanchette
57cb59a845 Merge branch 'master' into conditional-constraints 2022-08-13 14:20:41 -07:00
Henry Blanchette
fcce470d1e updated docs to reflect new warning 2022-08-12 23:08:00 -07:00
Iavor Diatchki
f77e5cc1c9 Merge remote-tracking branch 'origin/master' into functors-merge 
# Conflicts:
#	cryptol-remote-api/src/CryptolServer/Exceptions.hs
#	cryptol.cabal
#	docs/RefMan/_build/doctrees/BasicSyntax.doctree
#	docs/RefMan/_build/doctrees/BasicTypes.doctree
#	docs/RefMan/_build/doctrees/Expressions.doctree
#	docs/RefMan/_build/doctrees/Modules.doctree
#	docs/RefMan/_build/doctrees/OverloadedOperations.doctree
#	docs/RefMan/_build/doctrees/RefMan.doctree
#	docs/RefMan/_build/doctrees/TypeDeclarations.doctree
#	docs/RefMan/_build/doctrees/environment.pickle
#	docs/RefMan/_build/html/Modules.html
#	docs/RefMan/_build/html/searchindex.js
#	src/Cryptol/ModuleSystem.hs
#	src/Cryptol/ModuleSystem/Base.hs
#	src/Cryptol/ModuleSystem/Env.hs
#	src/Cryptol/ModuleSystem/InstantiateModule.hs
#	src/Cryptol/ModuleSystem/Monad.hs
#	src/Cryptol/Parser/Token.hs
#	src/Cryptol/Transform/AddModParams.hs
#	src/Cryptol/TypeCheck/Error.hs
#	src/Cryptol/TypeCheck/Infer.hs
#	src/Cryptol/TypeCheck/InferTypes.hs
 2022-08-12 17:50:56 +03:00