Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

'stack test' fails out of the box #1

Open
silky opened this issue Aug 26, 2021 · 2 comments
Open

'stack test' fails out of the box #1

silky opened this issue Aug 26, 2021 · 2 comments

Comments

@silky
Copy link

silky commented Aug 26, 2021

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
@Ziharrk
Copy link
Member

Ziharrk commented Aug 31, 2021

Ah sorry, we did not get a Notification, I'll get back to you soon.

@Ziharrk
Copy link
Member

Ziharrk commented Aug 31, 2021

Which Version of Z3 do you have installed. I know from experience that the package for debian/ubuntu is too old.
We use the package SBV, which requires a pretty new Version of Z3.
They suggest installing it directly from the repository releases (here).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@silky @Ziharrk