'stack test' fails out of the box #1
Description
I think the issue is my version of z3:
02:09 PM noon φ inversion-plugin (main) stack test 1 ↵
sandbox-0.1.0.0: unregistering (local file changes: /home/noon/dev/ext/inversion-plugin/.stack-work/install/x86_64-linux/60d3a5c3dd04c4b4e3d7c1f5e910...)
inversion-plugin> test (suite: tests)
sandbox > build (lib + exe)
inversion-plugin> Loaded package environment from /tmp/stack-08515061b9dd3efa/test-ghc-env
sandbox > Preprocessing library for sandbox-0.1.0.0..
sandbox > Building library for sandbox-0.1.0.0..
inversion-plugin> Loaded package environment from /tmp/stack-08515061b9dd3efa/test-ghc-env
inversion-plugin> [1 of 1] Compiling Data ( Data.hs, out/Data.o )
inversion-plugin> Loaded package environment from /tmp/stack-08515061b9dd3efa/test-ghc-env
inversion-plugin> Loaded package environment from /tmp/stack-08515061b9dd3efa/test-ghc-env
inversion-plugin> [1 of 2] Compiling Export ( Export.hs, out/Export.o )
sandbox > Preprocessing executable 'benchEx' for sandbox-0.1.0.0..
sandbox > Building executable 'benchEx' for sandbox-0.1.0.0..
sandbox > copy/register
sandbox > Installing library in /home/noon/dev/ext/inversion-plugin/.stack-work/install/x86_64-linux/60d3a5c3dd04c4b4e3d7c1f5e9100ffc5161000a4a0855d7b931c618838975a3/8.10.4/lib/x86_64-linux-ghc-8.10.4/sandbox-0.1.0.0-Gbl4rnRvrYXO3vUE9uy67
sandbox > Installing executable benchEx in /home/noon/dev/ext/inversion-plugin/.stack-work/install/x86_64-linux/60d3a5c3dd04c4b4e3d7c1f5e9100ffc5161000a4a0855d7b931c618838975a3/8.10.4/bin
sandbox > Registering library for sandbox-0.1.0.0..
inversion-plugin> [2 of 2] Compiling Import ( Import.hs, out/Import.o )
inversion-plugin> Loaded package environment from /tmp/stack-08515061b9dd3efa/test-ghc-env
inversion-plugin> Loaded package environment from /tmp/stack-08515061b9dd3efa/test-ghc-env
inversion-plugin> [1 of 2] Compiling ExportHaskell ( ExportHaskell.hs, out/ExportHaskell.o )
inversion-plugin> [2 of 2] Compiling ImportHaskell ( ImportHaskell.hs, out/ImportHaskell.o )
inversion-plugin>
inversion-plugin> ImportHaskell.hs:4:1: error:
inversion-plugin> Error! Module ‘ExportHaskell’ was not compiled with the Curry-Plugin and cannot be imported.
inversion-plugin> |
inversion-plugin> 4 | import ExportHaskell
inversion-plugin> | ^^^^^^^^^^^^^^^^^^^^
inversion-plugin> Loaded package environment from /tmp/stack-08515061b9dd3efa/test-ghc-env
inversion-plugin> Loaded package environment from /tmp/stack-08515061b9dd3efa/test-ghc-env
inversion-plugin> [1 of 2] Compiling InstanceExport ( InstanceExport.hs, out/InstanceExport.o )
inversion-plugin> [2 of 2] Compiling InstanceImport ( InstanceImport.hs, out/InstanceImport.o )
inversion-plugin> Loaded package environment from /tmp/stack-08515061b9dd3efa/test-ghc-env
inversion-plugin> Loaded package environment from /tmp/stack-08515061b9dd3efa/test-ghc-env
inversion-plugin> [1 of 1] Compiling PatternMatching ( PatternMatching.hs, out/PatternMatching.o )
inversion-plugin> Loaded package environment from /tmp/stack-08515061b9dd3efa/test-ghc-env
inversion-plugin> Loaded package environment from /tmp/stack-08515061b9dd3efa/test-ghc-env
inversion-plugin> [1 of 1] Compiling Record ( Record.hs, out/Record.o )
inversion-plugin> Loaded package environment from /tmp/stack-08515061b9dd3efa/test-ghc-env
inversion-plugin> Loaded package environment from /tmp/stack-08515061b9dd3efa/test-ghc-env
inversion-plugin> [1 of 1] Compiling Typeclass ( Typeclass.hs, out/Typeclass.o )
inversion-plugin>
inversion-plugin> Typeclass.hs:13:10: warning: [-Wmissing-methods]
inversion-plugin> • No explicit implementation for
inversion-plugin> ‘myNot’
inversion-plugin> • In the instance declaration for ‘Not Int’
inversion-plugin> |
inversion-plugin> 13 | instance Not Int where
inversion-plugin> | ^^^^^^^
inversion-plugin> Test case Data.hs: Pass
inversion-plugin> Test case Import.hs: Pass
inversion-plugin> Test case ImportHaskell.hs: Pass
inversion-plugin> Test case InstanceImport.hs: Pass
inversion-plugin> Test case PatternMatching.hs: Pass
inversion-plugin> Test case Record.hs: Pass
inversion-plugin> Test case Typeclass.hs: Pass
inversion-plugin> *** Failed! (after 1 test):
inversion-plugin> Exception:
inversion-plugin>
inversion-plugin> *** Data.SBV: Unexpected non-success response from Z3:
inversion-plugin> ***
inversion-plugin> *** Sent : (set-option :global-declarations true)
inversion-plugin> *** Expected : success
inversion-plugin> *** Received : (error "line 2 column 33: unknown parameter 'global_declarations'
inversion-plugin> *** Legal parameters are:
inversion-plugin> *** auto_config (bool) (default: true)
inversion-plugin> *** debug_ref_count (bool) (default: false)
inversion-plugin> *** dump_models (bool) (default: false)
inversion-plugin> *** memory_high_watermark (unsigned int) (default: 0)
inversion-plugin> *** memory_max_alloc_count (unsigned int) (default: 0)
inversion-plugin> *** memory_max_size (unsigned int) (default: 0)
inversion-plugin> *** model (bool) (default: true)
inversion-plugin> *** model_validate (bool) (default: false)
inversion-plugin> *** proof (bool) (default: false)
inversion-plugin> *** rlimit (unsigned int) (default: 4294967295)
inversion-plugin> *** smtlib2_compliant (bool) (default: false)
inversion-plugin> *** timeout (unsigned int) (default: 4294967295)
inversion-plugin> *** trace (bool) (default: false)
inversion-plugin> *** trace_file_name (string) (default: z3.log)
inversion-plugin> *** type_check (bool) (default: true)
inversion-plugin> *** unsat_core (bool) (default: false)
inversion-plugin> *** verbose (unsigned int) (default: 0)
inversion-plugin> *** warning (bool) (default: true)
inversion-plugin> *** well_sorted_check (bool) (default: false)")
inversion-plugin> ***
inversion-plugin> *** Exit code : ExitFailure (-15)
inversion-plugin> *** Executable: /usr/bin/z3
inversion-plugin> *** Options : -nw -in -smt2
inversion-plugin> ***
inversion-plugin> *** Reason : Backend solver reports it does not support this option.
inversion-plugin> *** Check the spelling, and if correct please report this as a
inversion-plugin> *** bug/feature request with the solver!
inversion-plugin> False
inversion-plugin> Test case is42Test: Fail "*** Failed! (after 1 test):\nException:\n \n ***
inversion-plugin> Data.SBV: Unexpected non-success response from Z3:\n ***\n *** Sent :
inversion-plugin> (set-option :global-declarations true)\n *** Expected : success\n *** Received
inversion-plugin> : (error \"line 2 column 33: unknown parameter 'global_declarations'\n ***
inversion-plugin> Legal parameters are:\n *** auto_config (bool) (default: true)\n ***
inversion-plugin> debug_ref_count (bool) (default: false)\n *** dump_models (bool) (default:
inversion-plugin> false)\n *** memory_high_watermark (unsigned int) (default: 0)\n ***
inversion-plugin> memory_max_alloc_count (unsigned int) (default: 0)\n *** memory_max_size
inversion-plugin> (unsigned int) (default: 0)\n *** model (bool) (default: true)\n ***
inversion-plugin> model_validate (bool) (default: false)\n *** proof (bool) (default: false)\n
inversion-plugin> *** rlimit (unsigned int) (default: 4294967295)\n *** smtlib2_compliant (bool)
inversion-plugin> (default: false)\n *** timeout (unsigned int) (default: 4294967295)\n ***
inversion-plugin> trace (bool) (default: false)\n *** trace_file_name (string) (default:
inversion-plugin> z3.log)\n *** type_check (bool) (default: true)\n *** unsat_core (bool)
inversion-plugin> (default: false)\n *** verbose (unsigned int) (default: 0)\n *** warning
inversion-plugin> (bool) (default: true)\n *** well_sorted_check (bool) (default: false)\")\n
inversion-plugin> ***\n *** Exit code : ExitFailure (-15)\n *** Executable: /usr/bin/z3\n ***
inversion-plugin> Options : -nw -in -smt2\n ***\n *** Reason : Backend solver reports it does
inversion-plugin> not support this option.\n *** Check the spelling, and if correct please
inversion-plugin> report this as a\n *** bug/feature request with the solver!\nFalse\n"
inversion-plugin> +++ OK, passed 100 tests; 17 discarded.
inversion-plugin> Test case lastTest: Pass
inversion-plugin> *** Failed! (after 2 tests and 2 shrinks):
inversion-plugin> Exception:
inversion-plugin>
inversion-plugin> *** Data.SBV: Unexpected non-success response from Z3:
inversion-plugin> ***
inversion-plugin> *** Sent : (set-option :global-declarations true)
inversion-plugin> *** Expected : success
inversion-plugin> *** Received : (error "line 2 column 33: unknown parameter 'global_declarations'
inversion-plugin> *** Legal parameters are:
inversion-plugin> *** auto_config (bool) (default: true)
inversion-plugin> *** debug_ref_count (bool) (default: false)
inversion-plugin> *** dump_models (bool) (default: false)
inversion-plugin> *** memory_high_watermark (unsigned int) (default: 0)
inversion-plugin> *** memory_max_alloc_count (unsigned int) (default: 0)
inversion-plugin> *** memory_max_size (unsigned int) (default: 0)
inversion-plugin> *** model (bool) (default: true)
inversion-plugin> *** model_validate (bool) (default: false)
inversion-plugin> *** proof (bool) (default: false)
inversion-plugin> *** rlimit (unsigned int) (default: 4294967295)
inversion-plugin> *** smtlib2_compliant (bool) (default: false)
inversion-plugin> *** timeout (unsigned int) (default: 4294967295)
inversion-plugin> *** trace (bool) (default: false)
inversion-plugin> *** trace_file_name (string) (default: z3.log)
inversion-plugin> *** type_check (bool) (default: true)
inversion-plugin> *** unsat_core (bool) (default: false)
inversion-plugin> *** verbose (unsigned int) (default: 0)
inversion-plugin> *** warning (bool) (default: true)
inversion-plugin> *** well_sorted_check (bool) (default: false)")
inversion-plugin> ***
inversion-plugin> *** Exit code : ExitFailure (-15)
inversion-plugin> *** Executable: /usr/bin/z3
inversion-plugin> *** Options : -nw -in -smt2
inversion-plugin> ***
inversion-plugin> *** Reason : Backend solver reports it does not support this option.
inversion-plugin> *** Check the spelling, and if correct please report this as a
inversion-plugin> *** bug/feature request with the solver!
inversion-plugin> [(0,0)]
inversion-plugin> 0
inversion-plugin> Test case lookupTestReverse: Fail "*** Failed! (after 2 tests and 2
inversion-plugin> shrinks):\nException:\n \n *** Data.SBV: Unexpected non-success response from
inversion-plugin> Z3:\n ***\n *** Sent : (set-option :global-declarations true)\n *** Expected :
inversion-plugin> success\n *** Received : (error \"line 2 column 33: unknown parameter
inversion-plugin> 'global_declarations'\n *** Legal parameters are:\n *** auto_config (bool)
inversion-plugin> (default: true)\n *** debug_ref_count (bool) (default: false)\n ***
inversion-plugin> dump_models (bool) (default: false)\n *** memory_high_watermark (unsigned int)
inversion-plugin> (default: 0)\n *** memory_max_alloc_count (unsigned int) (default: 0)\n ***
inversion-plugin> memory_max_size (unsigned int) (default: 0)\n *** model (bool) (default:
inversion-plugin> true)\n *** model_validate (bool) (default: false)\n *** proof (bool)
inversion-plugin> (default: false)\n *** rlimit (unsigned int) (default: 4294967295)\n ***
inversion-plugin> smtlib2_compliant (bool) (default: false)\n *** timeout (unsigned int)
inversion-plugin> (default: 4294967295)\n *** trace (bool) (default: false)\n ***
inversion-plugin> trace_file_name (string) (default: z3.log)\n *** type_check (bool) (default:
inversion-plugin> true)\n *** unsat_core (bool) (default: false)\n *** verbose (unsigned int)
inversion-plugin> (default: 0)\n *** warning (bool) (default: true)\n *** well_sorted_check
inversion-plugin> (bool) (default: false)\")\n ***\n *** Exit code : ExitFailure (-15)\n ***
inversion-plugin> Executable: /usr/bin/z3\n *** Options : -nw -in -smt2\n ***\n *** Reason :
inversion-plugin> Backend solver reports it does not support this option.\n *** Check the
inversion-plugin> spelling, and if correct please report this as a\n *** bug/feature request
inversion-plugin> with the solver!\n[(0,0)]\n0\n"
inversion-plugin> *** Failed! (after 1 test):
inversion-plugin> Exception:
inversion-plugin>
inversion-plugin> *** Data.SBV: Unexpected non-success response from Z3:
inversion-plugin> ***
inversion-plugin> *** Sent : (set-option :global-declarations true)
inversion-plugin> *** Expected : success
inversion-plugin> *** Received : (error "line 2 column 33: unknown parameter 'global_declarations'
inversion-plugin> *** Legal parameters are:
inversion-plugin> *** auto_config (bool) (default: true)
inversion-plugin> *** debug_ref_count (bool) (default: false)
inversion-plugin> *** dump_models (bool) (default: false)
inversion-plugin> *** memory_high_watermark (unsigned int) (default: 0)
inversion-plugin> *** memory_max_alloc_count (unsigned int) (default: 0)
inversion-plugin> *** memory_max_size (unsigned int) (default: 0)
inversion-plugin> *** model (bool) (default: true)
inversion-plugin> *** model_validate (bool) (default: false)
inversion-plugin> *** proof (bool) (default: false)
inversion-plugin> *** rlimit (unsigned int) (default: 4294967295)
inversion-plugin> *** smtlib2_compliant (bool) (default: false)
inversion-plugin> *** timeout (unsigned int) (default: 4294967295)
inversion-plugin> *** trace (bool) (default: false)
inversion-plugin> *** trace_file_name (string) (default: z3.log)
inversion-plugin> *** type_check (bool) (default: true)
inversion-plugin> *** unsat_core (bool) (default: false)
inversion-plugin> *** verbose (unsigned int) (default: 0)
inversion-plugin> *** warning (bool) (default: true)
inversion-plugin> *** well_sorted_check (bool) (default: false)")
inversion-plugin> ***
inversion-plugin> *** Exit code : ExitFailure (-15)
inversion-plugin> *** Executable: /usr/bin/z3
inversion-plugin> *** Options : -nw -in -smt2
inversion-plugin> ***
inversion-plugin> *** Reason : Backend solver reports it does not support this option.
inversion-plugin> *** Check the spelling, and if correct please report this as a
inversion-plugin> *** bug/feature request with the solver!
inversion-plugin> []
inversion-plugin> Test case lookupTestUnused: Fail "*** Failed! (after 1 test):\nException:\n \n
inversion-plugin> *** Data.SBV: Unexpected non-success response from Z3:\n ***\n *** Sent :
inversion-plugin> (set-option :global-declarations true)\n *** Expected : success\n *** Received
inversion-plugin> : (error \"line 2 column 33: unknown parameter 'global_declarations'\n ***
inversion-plugin> Legal parameters are:\n *** auto_config (bool) (default: true)\n ***
inversion-plugin> debug_ref_count (bool) (default: false)\n *** dump_models (bool) (default:
inversion-plugin> false)\n *** memory_high_watermark (unsigned int) (default: 0)\n ***
inversion-plugin> memory_max_alloc_count (unsigned int) (default: 0)\n *** memory_max_size
inversion-plugin> (unsigned int) (default: 0)\n *** model (bool) (default: true)\n ***
inversion-plugin> model_validate (bool) (default: false)\n *** proof (bool) (default: false)\n
inversion-plugin> *** rlimit (unsigned int) (default: 4294967295)\n *** smtlib2_compliant (bool)
inversion-plugin> (default: false)\n *** timeout (unsigned int) (default: 4294967295)\n ***
inversion-plugin> trace (bool) (default: false)\n *** trace_file_name (string) (default:
inversion-plugin> z3.log)\n *** type_check (bool) (default: true)\n *** unsat_core (bool)
inversion-plugin> (default: false)\n *** verbose (unsigned int) (default: 0)\n *** warning
inversion-plugin> (bool) (default: true)\n *** well_sorted_check (bool) (default: false)\")\n
inversion-plugin> ***\n *** Exit code : ExitFailure (-15)\n *** Executable: /usr/bin/z3\n ***
inversion-plugin> Options : -nw -in -smt2\n ***\n *** Reason : Backend solver reports it does
inversion-plugin> not support this option.\n *** Check the spelling, and if correct please
inversion-plugin> report this as a\n *** bug/feature request with the solver!\n[]\n"
inversion-plugin> Test suite tests failed
Completed 2 action(s).
Test suite failure for package inversion-plugin-1.0
tests: exited with: ExitFailure 1
Logs printed to console
02:16 PM noon φ inversion-plugin (main) z3 --version
Z3 version 4.4.1