Use smart constructor instead of VSeq

CHANGES.md

@@ -4,6 +4,11 @@
 
 ## Bug fixes
 
+* Fix #1437, enforce the VSeq invariant that it is not a sequence of bits.
+  Replaces the VSeq constructor with a view-only pattern, and smart constructors
+  `mkSeq` and `finSeq`.
+  ([#1437](https://github.com/GaloisInc/cryptol/issues/1437))
+
 * Fix #1740, removes duplicated width from word values.
   Note that since this changes the types, it may require changes to libraries
   depending on Cryptol.
@@ -24,6 +29,9 @@
 
 ## New features
 
+* Improved the naming convention for anonymous modules generated by the
+  module system ([#1810](https://github.com/GaloisInc/cryptol/issues/1810))
+
 * REPL command `:dumptests <FILE> <EXPR>` updated to write to stdout when
   invoked as `:dumptests - <EXPR>` allowing for easier experimentation and
   testing.

cry

@@ -20,6 +20,7 @@ Available commands:
   haddock                      Generate Haddock documentation
   test                         Run some tests (may take a while)
   quick-test                   Like "test" but run fewer tests by default
+  set-test-output              Copy test results to expected results
   rpc-test                     Run RPC server tests
   rpc-docs                     Check that the RPC documentation is up-to-date
   exe-path                     Print the location of the local executable
@@ -88,6 +89,16 @@ case $COMMAND in
       "${TESTS[@]}"
     ;;
 
+  set-test-output)
+    DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
+    FILE=$(mktemp)
+    pushd "$DIR/output"
+    find . -name '*.stdout*' -print0 | tar czf "$FILE" --null -T -
+    popd
+    tar xzvf "$FILE"
+    rm -rf "$FILE"
+  ;;
+
   rpc-test)
     echo Running RPC server tests
     DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"

cryptol-remote-api/cryptol-eval-server/Main.hs

@@ -41,12 +41,10 @@ import CryptolServer
 import CryptolServer.Call ( call )
 import CryptolServer.Data.Expression ( Expression )
 import CryptolServer.Data.Type ( JSONSchema )
-import CryptolServer.EvalExpr
-    ( evalExpressionDescr, evalExpression )
-import CryptolServer.ExtendSearchPath
-    ( extSearchPath, extSearchPathDescr )
-import CryptolServer.FocusedModule
-    ( focusedModuleDescr, focusedModule )
+import CryptolServer.EvalExpr (evalExpressionDescr, evalExpression)
+import CryptolServer.ExtendSearchPath (extSearchPath, extSearchPathDescr)
+import CryptolServer.FocusedModule (focusedModuleDescr, focusedModule)
+import CryptolServer.FocusModule (focusModule, focusModuleDescr)
 import CryptolServer.Names ( visibleNamesDescr, visibleNames )
 import CryptolServer.Modules ( visibleModulesDescr, visibleModules )
 import CryptolServer.TypeCheck ( checkType )
@@ -141,6 +139,10 @@ cryptolEvalMethods =
      "focused module"
      focusedModuleDescr
      focusedModule
+  , command
+     "focus module"
+     focusModuleDescr
+     focusModule
   , command
      "evaluate expression"
      evalExpressionDescr

cryptol-remote-api/cryptol-remote-api.cabal

@@ -76,8 +76,10 @@ library
     CryptolServer.ExtendSearchPath
     CryptolServer.FileDeps
     CryptolServer.FocusedModule
+    CryptolServer.FocusModule
     CryptolServer.Interrupt
     CryptolServer.LoadModule
+    CryptolServer.LoadProject
     CryptolServer.Modules
     CryptolServer.Names
     CryptolServer.Options

cryptol-remote-api/cryptol-remote-api/Main.hs

@@ -25,19 +25,21 @@ import CryptolServer.EvalExpr
     ( evalExpression, evalExpressionDescr )
 import CryptolServer.ExtendSearchPath
     ( extSearchPath, extSearchPathDescr )
-import CryptolServer.FocusedModule
-    ( focusedModule, focusedModuleDescr )
+import CryptolServer.FocusedModule (focusedModule, focusedModuleDescr)
+import CryptolServer.FocusModule (focusModule, focusModuleDescr)
 import CryptolServer.Interrupt
     ( interruptServer, interruptServerDescr )
 import CryptolServer.LoadModule
     ( loadFile, loadFileDescr, loadModule, loadModuleDescr )
+import CryptolServer.LoadProject ( loadProjectDescr, loadProject )
 import CryptolServer.Names ( visibleNames, visibleNamesDescr )
 import CryptolServer.Modules ( visibleModules, visibleModulesDescr )
 import CryptolServer.Sat ( proveSat, proveSatDescr )
 import CryptolServer.TypeCheck ( checkType, checkTypeDescr )
 import CryptolServer.Version ( version, versionDescr )
 import CryptolServer.FileDeps( fileDeps, fileDepsDescr )
 import Cryptol.REPL.Command (CommandResult, DocstringResult)
+import Cryptol.Project (ScanStatus, LoadProjectMode)
 
 main :: IO ()
 main =
@@ -61,7 +63,9 @@ serverDocs =
     [Doc.datatype @Expression,
      Doc.datatype @JSONSchema,
      Doc.datatype @DocstringResult,
-     Doc.datatype @CommandResult]
+     Doc.datatype @CommandResult,
+     Doc.datatype @ScanStatus,
+     Doc.datatype @LoadProjectMode]
   ]
 
 description :: String
@@ -110,6 +114,10 @@ cryptolMethods =
      "focused module"
      focusedModuleDescr
      focusedModule
+  , command
+     "focus module"
+     focusModuleDescr
+     focusModule
   , command
      "evaluate expression"
      evalExpressionDescr
@@ -138,6 +146,10 @@ cryptolMethods =
      "check docstrings"
      checkDocstringsDescr
      checkDocstrings
+  , command
+     "load project"
+     loadProjectDescr
+     loadProject
   , notification
      "interrupt"
      interruptServerDescr

cryptol-remote-api/docs/Cryptol.rst

@@ -272,6 +272,50 @@ The result of executing a single REPL command.
 
 
 
+.. _ScanStatus:
+ScanStatus
+~~~~~~~~~~
+
+List of module names and status of each.
+
+
+``scanned``
+  This file was successfully parsed and contains a change status.
+
+
+
+``invalid_module``
+  This file could not be parsed an analyzed due to syntax issues.
+
+
+
+``invalid_dep``
+  This file depends on a module that was not able to be loaded.
+
+
+
+.. _LoadProjectMode:
+LoadProjectMode
+~~~~~~~~~~~~~~~
+
+
+
+
+``modified``
+  Load modified files and files that depend on modified files
+
+
+
+``untested``
+  Load files that do not have a current test result
+
+
+
+``refresh``
+  Reload all files in the project discarding the cache results
+
+
+
 
 Methods
 -------
@@ -548,6 +592,27 @@ Return fields
 
 
 
+focus module (command)
+~~~~~~~~~~~~~~~~~~~~~~
+
+Focus the specified module (by name).
+
+Parameter fields
+++++++++++++++++
+
+
+``module name``
+  Name of module to focus.
+
+
+
+Return fields
++++++++++++++
+
+No return fields
+
+
+
 evaluate expression (command)
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
@@ -817,6 +882,40 @@ Return fields
 
 
 
+load project (command)
+~~~~~~~~~~~~~~~~~~~~~~
+
+Load project returning a list of all the modules and whether they have changed since the last load
+
+Parameter fields
+++++++++++++++++
+
+
+``path``
+  Path to directory containing the project
+
+
+
+``mode``
+  One of the modes described at :ref:`LoadProjectMode <LoadProjectMode>`.
+
+
+
+Return fields
++++++++++++++
+
+
+``scan_status``
+  List of module name and :ref:` scan status <ScanStatus>`.
+
+
+
+``test_results``
+  List of module name and cached test result.
+
+
+
+
 interrupt (notification)
 ~~~~~~~~~~~~~~~~~~~~~~~~
 

cryptol-remote-api/python/CHANGELOG.md

@@ -5,6 +5,12 @@
 * Add `modules` command to return the modules, submodules and associated
   documentation for them.
 
+* Add `focus module` command to set the current module for evaluation
+  and running tests.
+
+* Add `check docstrings` to run the docstring tests on the currently
+  focused module.
+
 ## 3.2.1 -- 2024-08-18
 
 * Require building with `argo-client-0.0.13` or later. `argo-client-0.0.13` uses

cryptol-remote-api/python/cryptol/commands.py

@@ -317,6 +317,18 @@ def process_result(self, res : Any) -> Any:
         return res
 
 
+class CryptolFocusModule(argo.Command):
+    def __init__(self, connection : HasProtocolState, name: str, timeout: Optional[float]) -> None:
+        super(CryptolFocusModule, self).__init__(
+            'focus module',
+            {'module name': name},
+            connection,
+            timeout=timeout
+        )
+
+    def process_result(self, res : Any) -> Any:
+        return res
+
 class CryptolVersion(argo.Command):
     def __init__(self, connection : HasProtocolState, timeout: Optional[float]) -> None:
         super(CryptolVersion, self).__init__(
@@ -365,3 +377,15 @@ def __init__(self, connection : HasProtocolState, timeout: Optional[float]) -> N
 
     def process_result(self, res : Any) -> Any:
         return res
+
+class CryptolLoadProject(argo.Command):
+    def __init__(self, connection : HasProtocolState, path: str, mode: str, timeout: Optional[float]) -> None:
+        super(CryptolLoadProject, self).__init__(
+            'load project',
+            {"path": path, "mode": mode},
+            connection,
+            timeout=timeout
+        )
+
+    def process_result(self, res : Any) -> Any:
+        return res

cryptol-remote-api/python/cryptol/connection.py

@@ -213,6 +213,18 @@ def check_docstrings(self, timeout: Optional[float] = None) -> argo.Command:
         self.most_recent_result = CryptolCheckDocstrings(self, timeout)
         return self.most_recent_result
 
+    def load_project(self, path: str, mode: str, *, timeout: Optional[float] = None) -> argo.Command:
+        """Load project. In refresh mode all of the project modules are loaded.
+        Otherwise only the modules affected by a change are loaded.
+
+        :param path: Path to project root
+        :param mode: "modified", "untested", "refresh"
+        :param timeout: Optional timeout for this request (in seconds).
+        """
+        timeout = timeout if timeout is not None else self.timeout
+        self.most_recent_result = CryptolLoadProject(self, path, mode, timeout)
+        return self.most_recent_result
+
     def load_module(self, module_name : str, *, timeout:Optional[float] = None) -> argo.Command:
         """Load a Cryptol module, like ``:module`` at the Cryptol REPL.
 
@@ -222,13 +234,13 @@ def load_module(self, module_name : str, *, timeout:Optional[float] = None) -> a
         self.most_recent_result = CryptolLoadModule(self, module_name, timeout)
         return self.most_recent_result
 
-    def file_deps(self, name : str, isFile : bool, *, timeout:Optional[float] = None) -> argo.Command:
+    def file_deps(self, name : str, is_file: bool, *, timeout:Optional[float] = None) -> argo.Command:
         """Get information about a module or a file.
 
         :param timeout: Optional timeout for this request (in seconds).
         """
         timeout = timeout if timeout is not None else self.timeout
-        self.most_recent_result = CryptolFileDeps(self, name, isFile, timeout)
+        self.most_recent_result = CryptolFileDeps(self, name, is_file, timeout)
         return self.most_recent_result
 
     def eval_raw(self, expression : Any, *, timeout:Optional[float] = None) -> argo.Command:
@@ -438,6 +450,15 @@ def focused_module(self, *, timeout:Optional[float] = None) -> argo.Command:
         self.most_recent_result = CryptolFocusedModule(self, timeout)
         return self.most_recent_result
 
+    def focus_module(self, name: str, *, timeout:Optional[float] = None) -> argo.Command:
+        """Focus on an already loaded module.
+
+        :param name: Name of the module.
+        :param timeout: Optional timeout for this request (in seconds)."""
+        timeout = timeout if timeout is not None else self.timeout
+        self.most_recent_result = CryptolFocusModule(self, name, timeout)
+        return self.most_recent_result
+
     def version(self, *, timeout:Optional[float] = None) -> argo.Command:
         """Returns version information about the Cryptol server.
 

cryptol-remote-api/python/cryptol/single_connection.py

@@ -131,6 +131,16 @@ def load_file(filename : str, *, timeout:Optional[float] = None) -> None:
     """
     __get_designated_connection().load_file(filename, timeout=timeout)
 
+def load_project(path : str, mode: str, *, timeout:Optional[float] = None) -> Any:
+    """Load project. In refresh mode all of the project modules are loaded.
+    Otherwise only the modules affected by a change are loaded.
+    """
+    return __get_designated_connection().load_project(path, mode, timeout=timeout)
+
+def check_docstrings(*, timeout:Optional[float] = None) -> Any:
+    """Check loaded module docstrings."""
+    return __get_designated_connection().check_docstrings(timeout=timeout)
+
 def load_module(module_name : str, *, timeout:Optional[float] = None) -> None:
     """Load a Cryptol module, like ``:module`` at the Cryptol REPL."""
     __get_designated_connection().load_module(module_name, timeout=timeout)
@@ -240,6 +250,10 @@ def focused_module(*, timeout:Optional[float] = None) -> cryptoltypes.CryptolMod
     """Returns the name and other information about the currently-focused module."""
     return __get_designated_connection().focused_module(timeout=timeout)
 
+def focus_module(name: str, *, timeout:Optional[float] = None) -> None:
+    """Focus on an already loaded module."""
+    __get_designated_connection().focus_module(name, timeout=timeout)
+
 def version(*, timeout:Optional[float] = None) -> CryptolVersionInfo:
     """Returns version information about the Cryptol server."""
     return __get_designated_connection().version(timeout=timeout)