1
1
mirror of https://github.com/anoma/juvix.git synced 2024-11-30 14:13:27 +03:00

Remove VampIR compile command and tests (#3104)

* Closes #2841 
* Moves the `vampir` compilation target under `dev`.
* Removes VampIR tests that require the external `vamp-ir` executable.
This commit is contained in:
Łukasz Czajka 2024-10-16 15:03:14 +02:00 committed by GitHub
parent c50ad06976
commit f1bb0e50d9
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
15 changed files with 19 additions and 481 deletions

View File

@ -10,7 +10,6 @@ import Commands.Compile.Cairo qualified as Cairo
import Commands.Compile.Native qualified as Native
import Commands.Compile.Options
import Commands.Compile.RiscZeroRust qualified as RiscZeroRust
import Commands.Compile.Vampir qualified as Vampir
import Commands.Compile.Wasi qualified as Wasi
runCommand :: (Members AppEffects r) => CompileCommand -> Sem r ()
@ -19,5 +18,4 @@ runCommand = \case
Wasi opts -> Wasi.runCommand opts
Anoma opts -> Anoma.runCommand opts
Cairo opts -> Cairo.runCommand opts
Vampir opts -> Vampir.runCommand opts
RiscZeroRust opts -> RiscZeroRust.runCommand opts

View File

@ -7,7 +7,6 @@ import Commands.Compile.Anoma.Options
import Commands.Compile.Cairo.Options
import Commands.Compile.Native.Options
import Commands.Compile.RiscZeroRust.Options
import Commands.Compile.Vampir.Options
import Commands.Compile.Wasi.Options
import Commands.Extra.NewCompile
import CommonOptions
@ -16,7 +15,6 @@ import Juvix.Config qualified as Config
data CompileCommand
= Native (NativeOptions 'InputMain)
| Wasi (WasiOptions 'InputMain)
| Vampir (VampirOptions 'InputMain)
| Anoma (AnomaOptions 'InputMain)
| Cairo (CairoOptions 'InputMain)
| RiscZeroRust (RiscZeroRustOptions 'InputMain)
@ -27,8 +25,7 @@ parseCompileCommand = commandTargetsHelper supportedTargets
supportedTargets :: [(CompileTarget, Parser CompileCommand)]
supportedTargets =
[ (AppTargetVampIR, Vampir <$> parseVampir),
(AppTargetAnoma, Anoma <$> parseAnoma),
[ (AppTargetAnoma, Anoma <$> parseAnoma),
(AppTargetCairo, Cairo <$> parseCairo),
(AppTargetNative64, Native <$> parseNative)
]

View File

@ -9,6 +9,7 @@ import Commands.Dev.DevCompile.Options
import Commands.Dev.DevCompile.Reg qualified as Reg
import Commands.Dev.DevCompile.Rust qualified as Rust
import Commands.Dev.DevCompile.Tree qualified as Tree
import Commands.Dev.DevCompile.Vampir qualified as Vampir
runCommand :: (Members AppEffects r) => DevCompileCommand -> Sem r ()
runCommand = \case
@ -19,3 +20,4 @@ runCommand = \case
Casm opts -> Casm.runCommand opts
Rust opts -> Rust.runCommand opts
NativeRust opts -> NativeRust.runCommand opts
Vampir opts -> Vampir.runCommand opts

View File

@ -7,6 +7,7 @@ import Commands.Dev.DevCompile.NativeRust.Options
import Commands.Dev.DevCompile.Reg.Options
import Commands.Dev.DevCompile.Rust.Options
import Commands.Dev.DevCompile.Tree.Options
import Commands.Dev.DevCompile.Vampir.Options
import CommonOptions
import Juvix.Config qualified as Config
@ -18,6 +19,7 @@ data DevCompileCommand
| Casm (CasmOptions 'InputMain)
| Rust (RustOptions 'InputMain)
| NativeRust (NativeRustOptions 'InputMain)
| Vampir (VampirOptions 'InputMain)
deriving stock (Data)
parseDevCompileCommand :: Parser DevCompileCommand
@ -28,7 +30,8 @@ parseDevCompileCommand =
commandReg,
commandTree,
commandCasm,
commandAsm
commandAsm,
commandVampir
]
<> [commandRust | Config.config ^. Config.configRust]
<> [commandNativeRust | Config.config ^. Config.configRust]
@ -82,3 +85,10 @@ commandNativeRust =
info
(NativeRust <$> parseNativeRust)
(progDesc "Compile to native executable through Rust")
commandVampir :: Mod CommandFields DevCompileCommand
commandVampir =
command "vampir" $
info
(Vampir <$> parseVampir)
(progDesc "Compile to VampIR")

View File

@ -1,7 +1,7 @@
module Commands.Compile.Vampir where
module Commands.Dev.DevCompile.Vampir where
import Commands.Base
import Commands.Compile.Vampir.Options
import Commands.Dev.DevCompile.Vampir.Options
import Commands.Extra.NewCompile
import Juvix.Compiler.Backend.VampIR.Translation qualified as VampIR

View File

@ -1,7 +1,7 @@
{-# LANGUAGE UndecidableInstances #-}
module Commands.Compile.Vampir.Options
( module Commands.Compile.Vampir.Options,
module Commands.Dev.DevCompile.Vampir.Options
( module Commands.Dev.DevCompile.Vampir.Options,
module Commands.Compile.CommonOptions,
)
where

View File

@ -15,5 +15,5 @@ toTestDescr = Normalize.toTestDescr' (const (coreVampIRAssertion (toStoredTransf
allTests :: TestTree
allTests =
testGroup
"JuvixCore VampIR positive tests"
"JuvixCore VampIR pipeline positive tests"
(map (mkTest . toTestDescr) Normalize.tests)

View File

@ -25,7 +25,6 @@ import Scope qualified
import Termination qualified
import Tree qualified
import Typecheck qualified
import VampIR qualified
slowTests :: IO TestTree
slowTests =
@ -42,7 +41,6 @@ slowTests =
return Compilation.allTests,
return Examples.allTests,
Casm.allTests,
VampIR.allTests,
return Anoma.allTests,
return Repl.allTests
]

View File

@ -1,18 +0,0 @@
module VampIR where
import Base
import VampIR.Compilation.Negative qualified as Negative
import VampIR.Compilation.Positive qualified as CompilationPositive
import VampIR.Core.Base
import VampIR.Core.Positive qualified as CorePositive
allTests :: IO TestTree
allTests =
withPrecondition precondition
. return
$ testGroup
"VampIR tests"
[ CorePositive.allTests,
CompilationPositive.allTests,
Negative.allTests
]

View File

@ -1,32 +0,0 @@
module VampIR.Compilation.Base where
import Base
import Core.VampIR.Base (coreVampIRAssertion')
import Juvix.Compiler.Core
import VampIR.Core.Base (VampirBackend (..), vampirAssertion')
vampirCompileAssertion :: Path Abs Dir -> Path Abs File -> Path Abs File -> (String -> IO ()) -> Assertion
vampirCompileAssertion root' mainFile dataFile step = do
step "Translate to JuvixCore"
entryPoint <- testDefaultEntryPointIO root' mainFile
PipelineResult {..} <- snd <$> testRunIO entryPoint upToStoredCore
let tab = computeCombinedInfoTable (_pipelineResult ^. coreResultModule)
coreVampIRAssertion' tab toVampIRTransformations mainFile dataFile step
vampirAssertion' entryPoint VampirHalo2 tab dataFile step
vampirCompileErrorAssertion ::
Path Abs Dir ->
Path Abs File ->
(String -> IO ()) ->
Assertion
vampirCompileErrorAssertion root' mainFile step = do
step "Translate to JuvixCore"
entryPoint <- testDefaultEntryPointIO root' mainFile
r <- testRunIOEither entryPoint upToStoredCore
case r of
Left _ -> return ()
Right res ->
let m = snd res ^. pipelineResult . coreResultModule
in case run $ runReader entryPoint $ runError @JuvixError $ toVampIR m of
Left _ -> return ()
Right _ -> assertFailure "no error"

View File

@ -1,37 +0,0 @@
module VampIR.Compilation.Negative where
import Base
import VampIR.Compilation.Base
data NegTest = NegTest
{ _name :: String,
_relDir :: Path Rel Dir,
_file :: Path Rel File
}
root :: Path Abs Dir
root = relToProject $(mkRelDir "tests/VampIR/negative")
testDescr :: NegTest -> TestDescr
testDescr NegTest {..} =
let tRoot = root <//> _relDir
file' = tRoot <//> _file
in TestDescr
{ _testName = _name,
_testRoot = tRoot,
_testAssertion = Steps $ vampirCompileErrorAssertion tRoot file'
}
allTests :: TestTree
allTests =
testGroup
"Juvix to VampIR compilation negative tests"
(map (mkTest . testDescr) tests)
tests :: [NegTest]
tests =
[ NegTest
"Test001: Missing comma"
$(mkRelDir ".")
$(mkRelFile "test001.juvix")
]

View File

@ -1,162 +0,0 @@
module VampIR.Compilation.Positive where
import Base
import VampIR.Compilation.Base
data PosTest = PosTest
{ _name :: String,
_dir :: Path Abs Dir,
_file :: Path Abs File,
_dataFile :: Path Abs File
}
makeLenses ''PosTest
fromTest :: PosTest -> TestTree
fromTest = mkTest . toTestDescr
root :: Path Abs Dir
root = relToProject $(mkRelDir "tests/VampIR/positive/Compilation")
toTestDescr :: PosTest -> TestDescr
toTestDescr PosTest {..} =
let tRoot = _dir
file' = _file
data' = _dataFile
in TestDescr
{ _testName = _name,
_testRoot = tRoot,
_testAssertion = Steps $ vampirCompileAssertion _dir file' data'
}
allTests :: TestTree
allTests =
testGroup
"Juvix to VampIR compilation positive tests"
(map (mkTest . toTestDescr) tests)
posTest :: String -> Path Rel Dir -> Path Rel File -> Path Rel File -> PosTest
posTest _name rdir rfile routfile =
let _dir = root <//> rdir
_file = _dir <//> rfile
_dataFile = root <//> routfile
in PosTest {..}
tests :: [PosTest]
tests =
[ posTest
"Test001: not function"
$(mkRelDir ".")
$(mkRelFile "test001.juvix")
$(mkRelFile "data/test001.json"),
posTest
"Test002: pattern matching"
$(mkRelDir ".")
$(mkRelFile "test002.juvix")
$(mkRelFile "data/test002.json"),
posTest
"Test003: inductive types"
$(mkRelDir ".")
$(mkRelFile "test003.juvix")
$(mkRelFile "data/test003.json"),
posTest
"Test004: arithmetic"
$(mkRelDir ".")
$(mkRelFile "test004.juvix")
$(mkRelFile "data/test004.json"),
posTest
"Test005: single-constructor inductive types"
$(mkRelDir ".")
$(mkRelFile "test005.juvix")
$(mkRelFile "data/test005.json"),
posTest
"Test006: higher-order inductive types"
$(mkRelDir ".")
$(mkRelFile "test006.juvix")
$(mkRelFile "data/test006.json"),
posTest
"Test007: let"
$(mkRelDir ".")
$(mkRelFile "test007.juvix")
$(mkRelFile "data/test007.json"),
posTest
"Test008: functions returning functions with variable capture"
$(mkRelDir ".")
$(mkRelFile "test008.juvix")
$(mkRelFile "data/test008.json"),
posTest
"Test009: applications with lets and cases in function position"
$(mkRelDir ".")
$(mkRelFile "test009.juvix")
$(mkRelFile "data/test009.json"),
posTest
"Test010: mid-square hashing (unrolled)"
$(mkRelDir ".")
$(mkRelFile "test010.juvix")
$(mkRelFile "data/test010.json"),
posTest
"Test011: recursion"
$(mkRelDir ".")
$(mkRelFile "test011.juvix")
$(mkRelFile "data/test011.json"),
posTest
"Test012: tail recursion"
$(mkRelDir ".")
$(mkRelFile "test012.juvix")
$(mkRelFile "data/test012.json"),
posTest
"Test013: tail recursion: Fibonacci numbers in linear time"
$(mkRelDir ".")
$(mkRelFile "test013.juvix")
$(mkRelFile "data/test013.json"),
posTest
"Test014: recursion through higher-order functions"
$(mkRelDir ".")
$(mkRelFile "test014.juvix")
$(mkRelFile "data/test014.json"),
posTest
"Test015: tail recursion through higher-order functions"
$(mkRelDir ".")
$(mkRelFile "test015.juvix")
$(mkRelFile "data/test015.json"),
posTest
"Test016: higher-order functions"
$(mkRelDir ".")
$(mkRelFile "test016.juvix")
$(mkRelFile "data/test016.json"),
posTest
"Test017: mutual recursion"
$(mkRelDir ".")
$(mkRelFile "test017.juvix")
$(mkRelFile "data/test017.json"),
posTest
"Test018: mid-square hashing"
$(mkRelDir ".")
$(mkRelFile "test018.juvix")
$(mkRelFile "data/test018.json"),
posTest
"Test019: polymorphism"
$(mkRelDir ".")
$(mkRelFile "test019.juvix")
$(mkRelFile "data/test019.json"),
posTest
"Test020: boolean target"
$(mkRelDir ".")
$(mkRelFile "test020.juvix")
$(mkRelFile "data/test020.json"),
posTest
"Test021: fast exponentiation (exponential unrolling)"
$(mkRelDir ".")
$(mkRelFile "test021.juvix")
$(mkRelFile "data/test021.json"),
posTest
"Test022: fast exponentiation"
$(mkRelDir ".")
$(mkRelFile "test022.juvix")
$(mkRelFile "data/test022.json"),
posTest
"Test023: permutative conversions"
$(mkRelDir ".")
$(mkRelFile "test023.juvix")
$(mkRelFile "data/test023.json")
]

View File

@ -1,133 +0,0 @@
module VampIR.Core.Base where
import Base
import Juvix.Compiler.Backend.VampIR.Translation qualified as VampIR
import Juvix.Compiler.Core
import Juvix.Prelude.Pretty
import System.Process qualified as P
data VampirBackend = VampirHalo2 | VampirPlonk
vampirAssertion :: VampirBackend -> Path Abs Dir -> Path Abs File -> Path Abs File -> (String -> IO ()) -> Assertion
vampirAssertion backend root mainFile dataFile step = do
step "Parse"
s <- readFile mainFile
case runParserMain mainFile defaultModuleId mempty s of
Left err -> assertFailure (show err)
Right tab -> do
entryPoint <- testDefaultEntryPointIO root mainFile
vampirAssertion' entryPoint backend tab dataFile step
precondition :: Assertion
precondition = do
assertCmdExists $(mkRelFile "vamp-ir")
vampirAssertion' :: EntryPoint -> VampirBackend -> InfoTable -> Path Abs File -> (String -> IO ()) -> Assertion
vampirAssertion' entryPoint backend tab dataFile step = do
withTempDir'
( \dirPath -> do
step "Translate to VampIR"
let vampirFile = dirPath <//> $(mkRelFile "program.pir")
case run (runReader entryPoint (runError @JuvixError (coreToVampIR (moduleFromInfoTable tab)))) of
Left err -> assertFailure (prettyString (fromJuvixError @GenericError err))
Right VampIR.Result {..} -> do
writeFileEnsureLn vampirFile _resultCode
vampirSetupArgs backend dirPath step
step "VampIR compile"
P.callProcess "vamp-ir" (compileArgs vampirFile dirPath backend)
step "VampIR prove"
P.callProcess "vamp-ir" (proveArgs dataFile dirPath backend)
step "VampIR verify"
P.callProcess "vamp-ir" (verifyArgs dirPath backend)
)
vampirSetupArgs :: VampirBackend -> Path Abs Dir -> (String -> IO ()) -> Assertion
vampirSetupArgs VampirHalo2 _ _ = return ()
vampirSetupArgs VampirPlonk dirPath step = do
step "VampIR setup parameters"
P.callProcess "vamp-ir" setupParamsArgs
where
setupParamsArgs =
[ "-q",
"plonk",
"setup",
"-m",
"9",
"-o",
toFilePath (dirPath <//> $(mkRelFile "params.pp"))
]
compileArgs :: Path Abs File -> Path Abs Dir -> VampirBackend -> [String]
compileArgs inputFile dirPath = \case
VampirHalo2 ->
[ "-q",
"halo2",
"compile",
"-s",
toFilePath inputFile,
"-o",
toFilePath (dirPath <//> $(mkRelFile "circuit.halo2"))
]
VampirPlonk ->
[ "-q",
"plonk",
"compile",
"-u",
toFilePath (dirPath <//> $(mkRelFile "params.pp")),
"-s",
toFilePath inputFile,
"-o",
toFilePath (dirPath <//> $(mkRelFile "circuit.plonk"))
]
proveArgs :: Path Abs File -> Path Abs Dir -> VampirBackend -> [String]
proveArgs dataFile dirPath = \case
VampirHalo2 ->
[ "-q",
"halo2",
"prove",
"-c",
toFilePath (dirPath <//> $(mkRelFile "circuit.halo2")),
"-o",
toFilePath (dirPath <//> $(mkRelFile "proof.halo2")),
"-i",
toFilePath dataFile
]
VampirPlonk ->
[ "-q",
"plonk",
"prove",
"-u",
toFilePath (dirPath <//> $(mkRelFile "params.pp")),
"-c",
toFilePath (dirPath <//> $(mkRelFile "circuit.plonk")),
"-o",
toFilePath (dirPath <//> $(mkRelFile "proof.plonk")),
"-i",
toFilePath dataFile
]
verifyArgs :: Path Abs Dir -> VampirBackend -> [String]
verifyArgs dirPath = \case
VampirHalo2 ->
[ "-q",
"halo2",
"verify",
"-c",
toFilePath (dirPath <//> $(mkRelFile "circuit.halo2")),
"-p",
toFilePath (dirPath <//> $(mkRelFile "proof.halo2"))
]
VampirPlonk ->
[ "-q",
"plonk",
"verify",
"-u",
toFilePath (dirPath <//> $(mkRelFile "params.pp")),
"-c",
toFilePath (dirPath <//> $(mkRelFile "circuit.plonk")),
"-p",
toFilePath (dirPath <//> $(mkRelFile "proof.plonk"))
]

View File

@ -1,57 +0,0 @@
module VampIR.Core.Positive where
import Base
import Core.Normalize.Positive (PosTest (..))
import Core.Normalize.Positive qualified as Normalize
import VampIR.Core.Base
fromTest :: PosTest -> TestTree
fromTest = mkTest . toTestDescr
toTestDescr :: PosTest -> TestDescr
toTestDescr = Normalize.toTestDescr' (vampirAssertion VampirHalo2)
toPlonkTestDescr :: PosTest -> TestDescr
toPlonkTestDescr = Normalize.toTestDescr' (vampirAssertion VampirPlonk)
allTests :: TestTree
allTests =
testGroup
"Core to VampIR translation positive tests"
( map (mkTest . toPlonkTestDescr . (over Normalize.name (++ " (plonk)"))) tests
++ map
(mkTest . toTestDescr)
( tests
++ ( Normalize.filterOutTests
( -- VampIR stack overflow
[ "Test020: functional queues",
"Test026: letrec"
]
++
-- recursion takes too long
[ "Test014: recursion",
"Test015: tail recursion",
"Test016: tail recursion: Fibonacci numbers in linear time",
"Test017: recursion through higher-order functions",
"Test018: tail recursion through higher-order functions",
"Test022: mutual recursion"
]
)
Normalize.tests
)
)
)
tests :: [PosTest]
tests =
[ PosTest
"Test001"
$(mkRelDir "translation")
$(mkRelFile "test001.jvc")
$(mkRelFile "data/test001.json"),
PosTest
"Test002"
$(mkRelDir "translation")
$(mkRelFile "test002.jvc")
$(mkRelFile "data/test002.json")
]

View File

@ -162,34 +162,6 @@ tests:
stdin: "[call [L [replace [RL [quote 0]] [@ S]]]]"
exit-status: 0
- name: target-vampir
command:
shell:
- bash
script: |
temp=$(mktemp -d)
trap 'rm -rf -- "$temp"' EXIT
testdir=$PWD/tests/VampIR/positive/Compilation
cd $temp
juvix --log-level error compile vampir $testdir/test001.juvix
grep -q 'VampIR runtime for Juvix (safe version)' test001.pir
stdout: ""
exit-status: 0
- name: target-varmpir-unsafe
command:
shell:
- bash
script: |
temp=$(mktemp -d)
trap 'rm -rf -- "$temp"' EXIT
testdir=$PWD/tests/VampIR/positive/Compilation
cd $temp
juvix --log-level error compile vampir $testdir/test001.juvix --unsafe
grep -q 'VampIR runtime for Juvix (unsafe version)' test001.pir
stdout: ""
exit-status: 0
- name: input-file-does-not-exist
command:
- juvix