search

ranjitjhala / sprite-lang

An tutorial-style implementation of liquid/refinement types for a subset of Ocaml/Reason.
BSD 3-Clause "New" or "Revised" License
146 stars 13 forks source link

unknown parameter 'model_partial' #3

Closed k4rtik closed 1 year ago

k4rtik commented 1 year ago

Hi @ranjitjhala

Thanks for this tutorial introduction to refinement types. When I try to run the example in README, I get the following error:

✗ stack exec -- sprite 8 test/L8/pos/listSet.re
Crash!: :1:1-1:1: Error
  crash: SMTLIB2 respSat = Error "line 4 column 27: unknown parameter 'model_partial', this is an old parameter name, invoke 'z3 -p' to obtain the new parameter list"

I am using the fork I made at https://github.com/k4rtik/sprite-lang to be able to run the code on my M1 machine. Specifically, I am on ghc 8.10.7, Z3 version 4.11.2, and liquid-fixpoint commit: 92e434da5653c5d75e1f6f1bd687bc0dc9d8acdf

k4rtik commented 1 year ago

I see this is also reported at https://github.com/ucsd-progsys/liquid-fixpoint/issues/622

k4rtik commented 1 year ago

Fixed by updating liquid-fixpoint, see https://github.com/k4rtik/sprite-lang/commit/69f32f091e1ea3d58bf07b818c7e249b2664cbcf#diff-0de01f189d384bfbe69e806ef70b1a425b27394dbe2a9d0e62ffd010dda86c03

ranjitjhala commented 1 year ago

Thanks Kartik - I just bumped the stack/cabal to update so this should go away!

On Wed, Jan 11, 2023 at 9:23 AM Kartik Singhal @.***> wrote:

Closed #3 https://urldefense.com/v3/__https://github.com/ranjitjhala/sprite-lang/issues/3__;!!Mih3wA!Ho_gWTPK07ajLLIfM_yEY0V9d1p_2rKLtPLYwFJz9zPOtIU-QBXlR9cPnrDjMEuSS_KZpwH_2f817KPnpFFWMBMy$ as completed.

— Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/ranjitjhala/sprite-lang/issues/3*event-8203891069__;Iw!!Mih3wA!Ho_gWTPK07ajLLIfM_yEY0V9d1p_2rKLtPLYwFJz9zPOtIU-QBXlR9cPnrDjMEuSS_KZpwH_2f817KPnpJa8Q79_$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OGXSUYNPJLZPV4GCOTWR3UCJANCNFSM6AAAAAATXO5KHY__;!!Mih3wA!Ho_gWTPK07ajLLIfM_yEY0V9d1p_2rKLtPLYwFJz9zPOtIU-QBXlR9cPnrDjMEuSS_KZpwH_2f817KPnpJlZ8pbD$ . You are receiving this because you were mentioned.Message ID: @.***>