264 Commits

Author	SHA1	Message	Date
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
Bretton	d933fa6307	FFI: Improve docs	2022-08-11 19:45:50 -07:00
Bretton	60a342ad9f	FFI: Improve docs	2022-08-11 14:56:43 -07:00
Bretton	0bc3bb74c5	FFI: Add docs	2022-08-11 12:26:48 -07:00
Henry Blanchette	eca8366659	rest of the docs stuff ... rest of the docs stuff [ci skip]	2022-08-11 12:25:37 -07:00
Henry Blanchette	5e0d8a8e5f	updated docs: constraint guads exhaustivity requirement	2022-08-11 12:12:00 -07:00
Henry Blanchette	2ecee7b782	docs for constraint guards	2022-08-11 12:02:06 -07:00
Iavor Diatchki	dfdbd1217a	Merge branch 'master' into functors-merge ... # Conflicts: # docs/RefMan/Modules.rst # 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/_sources/Modules.rst.txt # docs/RefMan/_build/html/searchindex.js	2022-08-04 14:46:28 +03:00
Iavor Diatchki	9d68dc91ae	Add a note that the documentation of parameterized modules ... is about the upcoming version	2022-08-04 14:40:33 +03:00
Iavor Diatchki	c8e499cc1e	Improvements to reference manual	2022-08-04 14:37:15 +03:00