Request Failed0

[hafizhmakmur]

This code fails to compile (stuck at "Verifying...") and gives "Request Failed0" instead. Is there anything wrong with the code?

PS: While I'm at it, I'm only able to do the quickSort assignment because I'm using assume (++). Is it really the intended way?

[ranjitjhala]

Thanks for posting this Hafizh! It seems to work fine on my laptop locally I get the result **** RESULT: UNSAFE ************************************************************ /Users/rjhala/tmp/Foo.hs:259:32-33: Error: Liquid Type Mismatch 259 | | ok = Just (M r c vs) ^^ Inferred type VV : (IntMeasure.Vector a##xo) not a subtype of Required type VV : {VV : (IntMeasure.Vector a##xo) | vDim VV == size xs} In Context xs : {v : [a##xo] | size v >= 0 && len v >= 0} so let me check and see why the web demo is complaining!

…

On Tue, May 26, 2020 at 11:57 PM Hafizh Afkar Makmur < ***@***.***> wrote: This code <http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1590562380_9269.hs> fails to compile and gives "Request Failed0" instead. Is there anything wrong with the code? PS: While I'm at it, I'm only able to do the quickSort assignment because I'm using assume (++). Is it really the intended way? — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell-tutorial/issues/97__;!!Mih3wA!UlRZASK-_Jot1SbUGV-sckF4llc1ijHvPRcJtbFWEcVtY-ty7dvcOute8iFmDj1z$>, or unsubscribe <https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OER7HVRJ5RRUN2F6Y3RTS2TZANCNFSM4NL24TLA__;!!Mih3wA!UlRZASK-_Jot1SbUGV-sckF4llc1ijHvPRcJtbFWEcVtY-ty7dvcOute8kE1VgO6$> .

[hafizhmakmur]

@ranjitjhala After some modifications of the code, somehow I have a code that not only runs forever on the web demo, but also runs forever on my own machine! My z3 just keeps hogging CPU and it's stuck at 12%. Any idea of why this happens? Also does my implementation of matFromList and txgo looks right? Thank you.

NB: I try to input my codes to the tutorial page and it passes safe and sound.