2 Pull requests merged by 2 people

• Change the naming convention for anonymous modules

  #1811 merged Feb 21, 2025

• Add project and docstring checking functions to cryptol-remote-api

  #1793 merged Feb 18, 2025

2 Pull requests opened by 2 people

• check if what4 adapter is present before setting timeout

  #1809 opened Feb 19, 2025

• Improve error messages, which mention module parameters.

  #1813 opened Feb 25, 2025

15 Issues closed by 3 people

• Core lint failure on well-typed term

  #1189 closed Feb 24, 2025

• Add a way to list the file dependencies of a Cryptol module

  #1332 closed Feb 21, 2025

• Don't panic on private module parameters

  #1187 closed Feb 21, 2025

• REPL evaluation doesn't work after interrupting prover with Ctrl-C

  #1167 closed Feb 21, 2025

• Document nested modules

  #1153 closed Feb 21, 2025

• User namable anonymous modules

  #1810 closed Feb 21, 2025

• Treat `prime` constraints as numeric during SMT typechecking

  #1657 closed Feb 20, 2025

• Parameterized modules redesign

  #815 closed Feb 19, 2025

• Type constraint failure messages could be more informative

  #865 closed Feb 19, 2025

• Parameterized module that extends another parameterized module

  #585 closed Feb 19, 2025

• Streamline Parameterized Module use

  #546 closed Feb 19, 2025

• :browse seems wrong when given parameters

  #689 closed Feb 19, 2025

• Documentation missing on backtick import of types

  #1042 closed Feb 19, 2025

• Rewrite the AES parameterized example to show off the new module system

  #1375 closed Feb 19, 2025

• Parameterized modules in the REPL

  #998 closed Feb 19, 2025

4 Issues opened by 1 person

• Incomplete reasoning about exponentiation: `2^^h + 2^^h - 2^^h` does not always simplify to `2^^h`

  #1812 opened Feb 24, 2025

• `proverTimeout` is broken for various SBV-based solvers

  #1808 opened Feb 18, 2025

• `proverTimeout` is broken for What4-based solvers

  #1807 opened Feb 18, 2025

• Drop CVC4 support

  #1806 opened Feb 18, 2025

9 Unresolved conversations

Sometimes conversations happen on old items that aren’t yet closed. Here is a list of all the Issues and Pull Requests with unresolved conversations.

• Use smart constructor instead of VSeq

  #1804 commented on Feb 24, 2025 • 20 new comments

• QordTrans theorem hangs when using cvc5

  #1805 commented on Feb 18, 2025 • 0 new comments

• properties in parameterized modules should not be accessible in instantiated modules by `:check` etc.

  #1646 commented on Feb 19, 2025 • 0 new comments

• The error messages have gotten worse

  #1560 commented on Feb 19, 2025 • 0 new comments

• Support `prime` in constraint guards

  #1658 commented on Feb 20, 2025 • 0 new comments

• Don't show funny numbers in error messages

  #782 commented on Feb 21, 2025 • 0 new comments

• Do not duplicate primitives' fixity declarations

  #634 commented on Feb 21, 2025 • 0 new comments

• Remove redundant checks in TC

  #823 commented on Feb 21, 2025 • 0 new comments

• Standardize on which `test-runner` to use

  #1177 commented on Feb 21, 2025 • 0 new comments