Merge branch 'dev' into support-ghc981

.github/actions/setup-haskell/action.yml

@@ -22,7 +22,7 @@ runs:
   steps:
     - id: setup-haskell
       name: Setup Haskell
-      uses: haskell/actions/setup@v2
+      uses: haskell-actions/setup@v2
       with:
         ghc-version: ${{ inputs.ghc-version }}
         cabal-version: ${{ inputs.cabal-version }}

.github/workflows/build-vehicle-python.yml

@@ -57,7 +57,7 @@ jobs:
           cabal-version: ${{ env.DEFAULT_CABAL_VERSION }}
 
       - name: Build wheel
-        uses: pypa/[email protected].2
+        uses: pypa/[email protected].4
         with:
           package-dir: "./vehicle-python"
           output-dir: "./vehicle-python/wheelhouse"

.github/workflows/ci.yml

@@ -65,8 +65,9 @@ jobs:
       - name: Download wheelhouse
         uses: actions/download-artifact@v4
         with:
-          pattern: "wheelhouse-*-*"
-          path: "wheelhouse"
+          pattern: wheelhouse-*-*
+          path: wheelhouse
+          merge-multiple: true
 
       - name: Publish to GitHub Releases
         uses: softprops/action-gh-release@v1
@@ -100,8 +101,9 @@ jobs:
       - name: Download wheelhouse
         uses: actions/download-artifact@v4
         with:
-          name: wheelhouse
+          name: wheelhouse-*-*
           path: wheelhouse
+          merge-multiple: true
 
       - name: Publish to PyPI
         uses: pypa/gh-action-pypi-publish@release/v1

.hlint.yaml

@@ -10,5 +10,3 @@
 - ignore: { name: Redundant return }
 - ignore: { name: Avoid lambda }
 - ignore: { name: Redundant <&> }
-# To generate a suitable file for HLint do:
-# $ hlint --default > .hlint.yaml

.pre-commit-config.yaml

@@ -46,7 +46,7 @@ repos:
       - id: isort
         args: ["--profile", "black", "--filter-files"]
   - repo: https://github.com/psf/black
-    rev: "23.12.1"
+    rev: "24.1.1"
     hooks:
       - id: black
   - repo: https://github.com/pre-commit/mirrors-mypy

CONTRIBUTING.md

@@ -329,6 +329,9 @@ The logging level can be changed by changing the command in the `test.json` file
 
 Some golden tests require external tools, such as the MarabouVerify test above. To run these tests, add `--test-option="--allowlist-externals=<external>"` to the test command, where `<external>` is the name of the external dependency, such as `Marabou`.
 
+Some golden tests diff extremely large files such as `.vcl-plan`s, for which the diff isn't very meaningful.
+In order to only display the change in size for a given file type, add `--test-option="--sizeOnly=<extension>"` to the test command, where `<extension>` is the extension of the chosen file type.
+
 ##### Adding golden tests
 
 To create a new golden test, you can use the `new-golden-test` command.
@@ -447,7 +450,7 @@ Ensure that [you have the source code](#getting-the-source) and that you have in
    vehicle --version
    ```
 
-   This should print `0.11.0`.
+   This should print `0.11.1`.
 
 ### Building the Vehicle Python bindings
 
@@ -570,14 +573,14 @@ Ensure that [you have the source code](#getting-the-source) and that you have in
    pipx run tox
    ```
 
-This creates the directory `dist` which contains "wheels", which are the binary distribution format for Python packages. These wheels will have file names such as `vehicle_lang-0.11.0-cp311-cp311-macosx_13_0_arm64`:
+This creates the directory `dist` which contains "wheels", which are the binary distribution format for Python packages. These wheels will have file names such as `vehicle_lang-0.11.1-cp311-cp311-macosx_13_0_arm64`:
 
 ```sh
 #   Supported
 #   Python   _____
 #   versions      \
 #                  vvvvvvvvvvv
-vehicle_lang-0.11.0-cp311-cp311-macosx_13_0_arm64
+vehicle_lang-0.11.1-cp311-cp311-macosx_13_0_arm64
 #                              ^^^^^^^^^^^^^^^^^
 #   Supported                /
 #   Operating System  ______/
@@ -722,7 +725,7 @@ Ensure that [you have the source code](#getting-the-source) and that you have in
    vehicle --version
    ```
 
-   This should print `0.11.0`.
+   This should print `0.11.1`.
 
 1. Check if your installation of the `vehicle_lang` package was successful.
 
@@ -917,11 +920,11 @@ The procedure to create a new release is:
    This creates the directory `dist` which contains "wheels", which are the binary distribution format for Python packages. If you're on macOS with an M1/M2 chipset, these look like:
 
    ```
-   vehicle_lang-0.11.0-cp310-cp310-macosx_13_0_arm64.whl
-   vehicle_lang-0.11.0-cp37-cp37m-macosx_13_0_arm64.whl
-   vehicle_lang-0.11.0-cp39-cp39-macosx_13_0_arm64.whl
-   vehicle_lang-0.11.0-cp311-cp311-macosx_13_0_arm64.whl
-   vehicle_lang-0.11.0-cp38-cp38-macosx_13_0_arm64.whl
+   vehicle_lang-0.11.1-cp310-cp310-macosx_13_0_arm64.whl
+   vehicle_lang-0.11.1-cp37-cp37m-macosx_13_0_arm64.whl
+   vehicle_lang-0.11.1-cp39-cp39-macosx_13_0_arm64.whl
+   vehicle_lang-0.11.1-cp311-cp311-macosx_13_0_arm64.whl
+   vehicle_lang-0.11.1-cp38-cp38-macosx_13_0_arm64.whl
    ```
 
    Run the following command to check each wheel's metadata:
@@ -942,7 +945,7 @@ The procedure to create a new release is:
 
    The release will be at a URL like:
 
-   <https://github.com/vehicle-lang/vehicle/releases/tag/v0.11.0>
+   <https://github.com/vehicle-lang/vehicle/releases/tag/v0.11.1>
 
 [vehicle-lang/vehicle]: https://github.com/vehicle-lang/vehicle
 [GHC]: https://www.haskell.org/ghc/

ChangeLog.md

@@ -2,6 +2,10 @@
 
 ## Version 0.12.0
 
+* Allow `@parameter`s to be used as network sizes.
+
+## Version 0.11.1
+
 * Fixed bug properties involving the comparison of abstract `Index` values would throw
   a `Something went wrong in query compilation` error.
 

bumpver.toml

@@ -1,5 +1,5 @@
 [bumpver]
-current_version = "v0.11.0"
+current_version = "v0.11.1"
 version_pattern = "vMAJOR.MINOR.PATCH"
 commit_message = "Bump version {old_version} -> {new_version}"
 commit = true

cabal.project.ghc-9.4.8

@@ -1,3 +1,4 @@
+
 -- Cabal project configuration file for GHC 9.4.8
 --
 -- See `cabal.project` for details.

tasty-golden-executable/src/Test/Tasty/Golden/Executable/Runner.hs

@@ -24,6 +24,7 @@ import Data.Functor ((<&>))
 import Data.List qualified as List (findIndices, splitAt, uncons)
 import Data.Maybe (fromMaybe, mapMaybe)
 import Data.Proxy (Proxy (..))
+import Data.Set (Set)
 import Data.Set qualified as Set
 import Data.String (IsString (..))
 import Data.Tagged (Tagged (..))
@@ -36,8 +37,8 @@ import Data.Traversable (for)
 import General.Extra.Diff (isBoth, mapDiff)
 import General.Extra.File (createDirectoryRecursive, listFilesRecursive, writeFileChanged)
 import General.Extra.NonEmpty qualified as NonEmpty (appendList, prependList, singleton)
-import System.Directory (copyFile, doesFileExist, removeFile)
-import System.FilePath (isAbsolute, isExtensionOf, makeRelative, stripExtension, (<.>), (</>))
+import System.Directory (copyFile, createDirectoryIfMissing, doesFileExist, removeFile)
+import System.FilePath (isAbsolute, isExtensionOf, makeRelative, stripExtension, takeDirectory, takeExtension, (<.>), (</>))
 import System.IO (IOMode (..), hFileSize, withFile)
 import System.IO.Temp (withSystemTempDirectory)
 import System.Process (CreateProcess (..), readCreateProcessWithExitCode, shell)
@@ -48,6 +49,7 @@ import Test.Tasty.Golden.Executable.TestSpec.Accept (Accept (..))
 import Test.Tasty.Golden.Executable.TestSpec.External (AllowlistExternals (..))
 import Test.Tasty.Golden.Executable.TestSpec.FilePattern (FilePattern, addExtension, asLiteral, glob, match)
 import Test.Tasty.Golden.Executable.TestSpec.Ignore (Ignore (..), IgnoreFiles (..), IgnoreLines (..))
+import Test.Tasty.Golden.Executable.TestSpec.SizeOnly (SizeOnlyExtensions, toSizeOnlyExtensionsSet)
 import Test.Tasty.Golden.Executable.TestSpec.TextPattern (strikeOut)
 import Test.Tasty.Golden.Executable.TestSpecs (TestSpecs (..), readTestSpecsFile, testSpecsFileName, writeTestSpecsFile)
 import Test.Tasty.Options (OptionDescription (..), OptionSet, lookupOption)
@@ -86,13 +88,14 @@ instance IsTest TestSpec where
               -- Diff stderr
               diffStderr maybeLooseEq stderr
               -- Diff produced files
-              diffTestProduced maybeLooseEq testSpecProduces (ignoreFiles <> lookupOption options)
+              diffTestProduced maybeLooseEq testSpecProduces (ignoreFiles <> lookupOption options) (lookupOption options)
 
   testOptions :: Tagged TestSpec [OptionDescription]
   testOptions =
     return
       [ Option (Proxy :: Proxy Accept),
         Option (Proxy :: Proxy AllowlistExternals),
+        Option (Proxy :: Proxy SizeOnlyExtensions),
         Option (Proxy :: Proxy IgnoreFiles),
         Option (Proxy :: Proxy IgnoreLines)
       ]
@@ -196,7 +199,7 @@ runTestRun cmd = TestT $ do
 diffStdout :: Maybe (Text -> Text -> Bool) -> Lazy.Text -> TestIO ()
 diffStdout maybeLooseEq actual = do
   golden <- readGoldenStdout
-  lift $ diffText (shortCircuitWithEq maybeLooseEq) golden actual
+  lift $ diffText (shortCircuitWithEq maybeLooseEq) Nothing golden actual
 
 -- | Update the standard output golden file.
 acceptStdout :: Lazy.Text -> TestIO ()
@@ -229,7 +232,7 @@ writeGoldenStdout contents = TestT $ do
 diffStderr :: Maybe (Text -> Text -> Bool) -> Lazy.Text -> TestIO ()
 diffStderr maybeLooseEq actual = do
   golden <- readGoldenStderr
-  lift $ diffText (shortCircuitWithEq maybeLooseEq) golden actual
+  lift $ diffText (shortCircuitWithEq maybeLooseEq) Nothing golden actual
 
 -- | Update the standard error golden file.
 acceptStderr :: Lazy.Text -> TestIO ()
@@ -259,10 +262,11 @@ writeGoldenStderr contents = TestT $ do
 -- | Compare the files produced by the test.
 --
 -- NOTE: The loose equality must extend equality.
-diffTestProduced :: Maybe (Text -> Text -> Bool) -> [FilePattern] -> IgnoreFiles -> TestIO ()
-diffTestProduced maybeLooseEq testProduces (IgnoreFiles testIgnores) = do
+diffTestProduced :: Maybe (Text -> Text -> Bool) -> [FilePattern] -> IgnoreFiles -> SizeOnlyExtensions -> TestIO ()
+diffTestProduced maybeLooseEq testProduces (IgnoreFiles testIgnores) sizeOnlyExtensions = do
   TestEnvironment {testDirectory, tempDirectory} <- getTestEnvironment
   let shortCircuitLooseEq = shortCircuitWithEq maybeLooseEq
+  let sizeOnlyExtensionsSet = toSizeOnlyExtensionsSet sizeOnlyExtensions
   -- Find the golden and actual files:
   goldenFiles <- findTestProducesGolden testProduces
   actualFiles <- findTestProducesActual testIgnores
@@ -279,13 +283,13 @@ diffTestProduced maybeLooseEq testProduces (IgnoreFiles testIgnores) = do
     let expectedFilesNotProduced = Set.toAscList $ Set.difference goldenFileSet actualFileSet
     for_ expectedFilesNotProduced $ tell . Just . expectedFileNotProduced
     -- Test for files which were produced but not expected:
-    let producedFilesNotExpected = Set.toAscList $ Set.difference goldenFileSet actualFileSet
+    let producedFilesNotExpected = Set.toAscList $ Set.difference actualFileSet goldenFileSet
     for_ producedFilesNotExpected $ tell . Just . producedFileNotExpected
     -- Diff the files which were produced and expected:
     for_ (Set.toAscList $ Set.intersection goldenFileSet actualFileSet) $ \file -> do
       let goldenFile = testDirectory </> file <.> "golden"
       let actualFile = tempDirectory </> file
-      catch (lift $ lift $ diffFile shortCircuitLooseEq goldenFile actualFile) $ \diff ->
+      catch (lift $ lift $ diffFile shortCircuitLooseEq sizeOnlyExtensionsSet goldenFile actualFile) $ \diff ->
         tell $ Just $ producedAndExpectedDiffer actualFile diff
 
   -- If errors were raised, throw them.
@@ -410,15 +414,17 @@ acceptTestProduced testProduces (IgnoreFiles testIgnores) = do
       when goldenFileExists $
         removeFile (testDirectory </> goldenFile)
   -- Copy the new .golden files:
-  lift $
+  lift $ do
     for_ actualFilesToCopy $ \actualFile -> do
       let goldenFile = actualFile <.> ".golden"
       goldenFileExists <- doesFileExist (testDirectory </> goldenFile)
       if goldenFileExists
         then do
           actualFileContents <- TextIO.readFile (tempDirectory </> actualFile)
           writeFileChanged (testDirectory </> goldenFile) actualFileContents
-        else do copyFile (tempDirectory </> actualFile) (testDirectory </> actualFile <.> ".golden")
+        else do
+          createDirectoryIfMissing True (takeDirectory (testDirectory </> actualFile))
+          copyFile (tempDirectory </> actualFile) (testDirectory </> actualFile <.> ".golden")
   return ()
 
 -- | Find the actual files produced by the test command.
@@ -485,23 +491,28 @@ fileSizeCutOffBytes = 100000
 -- | Compare two files.
 --
 -- NOTE: The loose equality must extend equality.
-diffFile :: (Text -> Text -> Bool) -> FilePath -> FilePath -> IO ()
-diffFile eq golden actual = do
+diffFile :: (Text -> Text -> Bool) -> Set String -> FilePath -> FilePath -> IO ()
+diffFile eq sizeOnlyExtensions golden actual = do
   withFile golden ReadMode $ \goldenHandle -> do
     goldenSize <- hFileSize goldenHandle
     goldenContents <- LazyIO.hGetContents goldenHandle
     withFile actual ReadMode $ \actualHandle -> do
       actualSize <- hFileSize actualHandle
+      let sizeDiff = makeSizeOnlyDiff goldenSize actualSize
+      let sizeOnly = Set.member (takeExtension actual) sizeOnlyExtensions
+      let maybeSizeDiff = if sizeOnly then Just sizeDiff else Nothing
       actualContents <- LazyIO.hGetContents actualHandle
       if max goldenSize actualSize < fileSizeCutOffBytes
-        then diffText eq goldenContents actualContents
-        else when (goldenContents /= actualContents) $ throw (NoDiff "file too big")
+        then diffText eq maybeSizeDiff goldenContents actualContents
+        else
+          when (goldenContents /= actualContents) $
+            throw (NoDiff ("file too big to diff but contents not equal. " <> sizeDiff))
 
 -- | Compare two texts.
 --
 -- NOTE: The loose equality must extend equality.
-diffText :: (Text -> Text -> Bool) -> Lazy.Text -> Lazy.Text -> IO ()
-diffText eq golden actual = do
+diffText :: (Text -> Text -> Bool) -> Maybe String -> Lazy.Text -> Lazy.Text -> IO ()
+diffText eq maybeSizeDiff golden actual = do
   -- Lazily split the golden and actual texts into lines
   let goldenLines = Lazy.toStrict <$> Lazy.lines golden
   let actualLines = Lazy.toStrict <$> Lazy.lines actual
@@ -510,7 +521,9 @@ diffText eq golden actual = do
   -- If both files are the same, the diff should be just "Both":
   unless (all isBoth groupedDiff) $
     throw $
-      Diff (ppDiff $ mapDiff (Text.unpack <$>) <$> groupedDiff)
+      Diff $ case maybeSizeDiff of
+        Nothing -> ppDiff $ mapDiff (Text.unpack <$>) <$> groupedDiff
+        Just sizeDiff -> sizeDiff
   return ()
 
 -- | Make a loose equality which ignores text matching the provided text patterns.
@@ -522,3 +535,12 @@ makeLooseEq (IgnoreLines patterns) golden actual = strikeOutAll golden == strike
 -- | Make a loose equality which short-circuits using equality.
 shortCircuitWithEq :: (Eq a) => Maybe (a -> a -> Bool) -> a -> a -> Bool
 shortCircuitWithEq maybeEq x y = x == y || maybe False (\eq -> x `eq` y) maybeEq
+
+makeSizeOnlyDiff :: Integer -> Integer -> String
+makeSizeOnlyDiff goldenSize actualSize =
+  "< expected "
+    <> show goldenSize
+    <> " bytes\n"
+    <> "> produced "
+    <> show actualSize
+    <> " bytes"

tasty-golden-executable/src/Test/Tasty/Golden/Executable/TestSpec/SizeOnly.hs

@@ -0,0 +1,64 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+
+module Test.Tasty.Golden.Executable.TestSpec.SizeOnly
+  ( SizeOnlyExtension (..),
+    SizeOnlyExtensions (..),
+    toSizeOnlyExtensionsSet,
+  )
+where
+
+import Data.Aeson.Types (FromJSON (..), Parser, ToJSON (..), Value, typeMismatch)
+import Data.Aeson.Types qualified as Value (Value (..))
+import Data.Data (Typeable)
+import Data.Set (Set)
+import Data.Set qualified as Set (fromList)
+import Data.String (IsString (..))
+import Data.Tagged (Tagged)
+import Data.Text qualified as Text
+import Test.Tasty.Options (IsOption (..), safeRead)
+
+-- | Extension for which only diffs should show the size.
+newtype SizeOnlyExtension = SizeOnlyExtension {extension :: FilePath}
+  deriving (Eq, Ord, Typeable)
+
+instance Show SizeOnlyExtension where
+  show :: SizeOnlyExtension -> String
+  show (SizeOnlyExtension programName) = programName
+
+instance Read SizeOnlyExtension where
+  readsPrec :: Int -> ReadS SizeOnlyExtension
+  readsPrec _prec programName = [(SizeOnlyExtension programName, "")]
+
+instance IsString SizeOnlyExtension where
+  fromString :: String -> SizeOnlyExtension
+  fromString = SizeOnlyExtension
+
+instance FromJSON SizeOnlyExtension where
+  parseJSON :: Value -> Parser SizeOnlyExtension
+  parseJSON (Value.String name) = return $ SizeOnlyExtension (Text.unpack name)
+  parseJSON value = typeMismatch "String" value
+
+instance ToJSON SizeOnlyExtension where
+  toJSON :: SizeOnlyExtension -> Value
+  toJSON = toJSON . extension
+
+newtype SizeOnlyExtensions = SizeOnlyExtensions [SizeOnlyExtension]
+  deriving (Eq, Ord, Show, Typeable, Semigroup, Monoid)
+
+instance IsOption SizeOnlyExtensions where
+  defaultValue :: SizeOnlyExtensions
+  defaultValue = mempty
+
+  parseValue :: String -> Maybe SizeOnlyExtensions
+  parseValue input = SizeOnlyExtensions <$> traverse safeRead names
+    where
+      names = Text.unpack . Text.strip <$> Text.splitOn "," (Text.pack input)
+
+  optionName :: Tagged SizeOnlyExtensions String
+  optionName = return "sizeOnly"
+
+  optionHelp :: Tagged SizeOnlyExtensions String
+  optionHelp = return "A list of file extensions for which diffs should only display the sizes of the old and new files."
+
+toSizeOnlyExtensionsSet :: SizeOnlyExtensions -> Set String
+toSizeOnlyExtensionsSet (SizeOnlyExtensions exts) = Set.fromList (fmap extension exts)

tasty-golden-executable/tasty-golden-executable.cabal

@@ -44,6 +44,7 @@ library
     Test.Tasty.Golden.Executable.TestSpec.External
     Test.Tasty.Golden.Executable.TestSpec.FilePattern
     Test.Tasty.Golden.Executable.TestSpec.Ignore
+    Test.Tasty.Golden.Executable.TestSpec.SizeOnly
     Test.Tasty.Golden.Executable.TestSpec.TextPattern
     Test.Tasty.Golden.Executable.TestSpec.Timeout
     Test.Tasty.Golden.Executable.TestSpecs