Several Issues when trying to use LiquidHaskell: unknown constant e-14 and stack overflow #1762
Comments
|
Changing: to: seemed to work around 'Issue#3'. 'z3' grew to a size of 43GB last I looked, it took a couple of days. Are there any Options or Pragmas that would be useful in this situation? |
|
Wow, not clear - I suspect SMT support for floats is quite finicky. It
would be great if you could:
1. Paste or send the /.liquid/file.smt2 file that LH generates
2. Just run z3 on it
3. Send it over so we can see if there are some options that might help?
…On Sat, Sep 26, 2020 at 10:03 PM Nathan Waivio ***@***.***> wrote:
Changing:
-- | 'tol' currently 128*eps
tol :: Cl3
{-# INLINE tol #-}
tol = R 1.4210854715202004e-14
tol' :: Double
{-# INLINE tol' #-}
tol' = 1.4210854715202004e-14
to:
-- | 'tol' currently 128*eps
tol :: Cl3
{-# INLINE tol #-}
tol = R 0.0
tol' :: Double
{-# INLINE tol' #-}
tol' = 0.0
seemed to work around 'Issue#3'.
'z3' grew to a size of 43GB last I looked, it took a couple of days.
Are there any Options or Pragmas that would be useful in this situation?
—
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/issues/1762*issuecomment-699585996__;Iw!!Mih3wA!RCC4AVftn8i8jQLL8DMyyUttH-yAAbyN3Ha-mlVgCl6E9hTV7c6tv_w6wu4dPJ6N$>,
or unsubscribe
<https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OGRXKCB4LV5UBGZR2TSH3BRZANCNFSM4RVGIFRQ__;!!Mih3wA!RCC4AVftn8i8jQLL8DMyyUttH-yAAbyN3Ha-mlVgCl6E9hTV7c6tv_w6wmcfn68T$>
.
|
|
Ok, Will do. It might take awhile until I can get the data because I'm away from my workstation for a month or so. |
|
Got the same issue for my playground project https://github.com/NCrashed/asteroids-arena/blob/master/haskell/asteroids/src/Game/Asteroids/World/Timer.hs#L30 I get: smt2 file: |
|
Perhaps, this is due http://hackage.haskell.org/package/clock-0.8/docs/src/System.Clock.html#toNanoSecs as it uses constant |
|
Interesting is there a snippet of code with which to reproduce? Will take a
look!
…On Wed, Dec 2, 2020 at 6:15 PM Anton Gushcha ***@***.***> wrote:
Perhaps, this is due
http://hackage.haskell.org/package/clock-0.8/docs/src/System.Clock.html#toNanoSecs
<https://urldefense.com/v3/__http://hackage.haskell.org/package/clock-0.8/docs/src/System.Clock.html*toNanoSecs__;Iw!!Mih3wA!SSjpIQSvhy9ZTHss-fzeEoBWgObZNn6w_EvznhZIO3W-5WdVwAcXYBwXmlHbYdb8$>
as it uses constant s2ns = 10^9.
—
You are receiving this because you commented.
Reply to this email directly, view it on GitHub
<https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/issues/1762*issuecomment-737615938__;Iw!!Mih3wA!SSjpIQSvhy9ZTHss-fzeEoBWgObZNn6w_EvznhZIO3W-5WdVwAcXYBwXmoP6CunL$>,
or unsubscribe
<https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OBLUBMO5SKP6AWMY73SS3YEDANCNFSM4RVGIFRQ__;!!Mih3wA!SSjpIQSvhy9ZTHss-fzeEoBWgObZNn6w_EvznhZIO3W-5WdVwAcXYBwXmmIlTkPT$>
.
|
NCrashed
added a commit
to NCrashed/liquid-test
that referenced
this issue
Dec 3, 2020
|
Minimal example (from https://github.com/NCrashed/liquid-test/blob/master/src/Liquid/Test/Assert.hs#L5) Got: smt2: |
|
Perfect thanks, this should help fix!
…On Thu, Dec 3, 2020 at 4:28 AM Anton Gushcha ***@***.***> wrote:
Minimal example (from
https://github.com/NCrashed/liquid-test/blob/master/src/Liquid/Test/Assert.hs#L5
<https://urldefense.com/v3/__https://github.com/NCrashed/liquid-test/blob/master/src/Liquid/Test/Assert.hs*L5__;Iw!!Mih3wA!Wj3YAU1WVGVo-UMl1meMIjFpEMNlPfD7CK5b0KZAcw1UFWkiPX_Kaw1n0V2e-mb9$>
)
spooky :: Float
spooky = 1 / 1000000000
Got:
**** LIQUID: ERROR :1:1-1:1: Error
crash: SMTLIB2 respSat = Error "line 286 column 150: unknown constant e9"
smt2:
(set-option :auto-config false)
(set-option :model true)
(set-option :model.partial false)
(set-option :smt.mbqi false)
(define-sort Str () Int)
(declare-fun strLen (Str) Int)
(declare-fun subString (Str Int Int) Str)
(declare-fun concatString (Str Str) Str)
(define-sort Elt () Int)
(define-sort LSet () (Array Elt Bool))
(define-fun smt_set_emp () LSet ((as const LSet) false))
(define-fun smt_set_mem ((x Elt) (s LSet)) Bool (select s x))
(define-fun smt_set_add ((s LSet) (x Elt)) LSet (store s x true))
(define-fun smt_set_cup ((s1 LSet) (s2 LSet)) LSet ((_ map or) s1 s2))
(define-fun smt_set_cap ((s1 LSet) (s2 LSet)) LSet ((_ map and) s1 s2))
(define-fun smt_set_com ((s LSet)) LSet ((_ map not) s))
(define-fun smt_set_dif ((s1 LSet) (s2 LSet)) LSet (smt_set_cap s1 (smt_set_com s2)))
(define-fun smt_set_sub ((s1 LSet) (s2 LSet)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
(define-sort Map () (Array Elt Elt))
(define-fun smt_map_sel ((m Map) (k Elt)) Elt (select m k))
(define-fun smt_map_sto ((m Map) (k Elt) (v Elt)) Map (store m k v))
(define-fun smt_map_cup ((m1 Map) (m2 Map)) Map ((_ map (+ (Elt Elt) Elt)) m1 m2))
(define-fun smt_map_def ((v Elt)) Map ((as const (Map)) v))
(define-fun bool_to_int ((b Bool)) Int (ite b 1 0))
(define-fun Z3_OP_MUL ((x Int) (y Int)) Int (* x y))
(define-fun Z3_OP_DIV ((x Int) (y Int)) Int (div x y))
(declare-fun GHC.Base.id () Int)
(declare-fun cast_as_int () Int)
(declare-fun GHC.Real.rem () Int)
(declare-fun GHC.List.init () Int)
(declare-fun addrLen () Int)
(declare-fun papp5 () Int)
(declare-fun GHC.List.iterate () Int)
(declare-fun x_Tuple21 () Int)
(declare-fun GHC.Classes.$61$$61$ () Int)
(declare-fun GHC.Types.C$35$ () Int)
(declare-fun GHC.List.drop () Int)
(declare-fun Data.Foldable.length () Int)
(declare-fun x_Tuple33 () Int)
(declare-fun GHC.Types.LT () Int)
(declare-fun GHC.List.replicate () Int)
(declare-fun GHC.List.zipWith () Int)
(declare-fun GHC.Classes.$62$$61$ () Int)
(declare-fun GHC.Types.F$35$ () Int)
(declare-fun GHC.Num.fromInteger () Int)
(declare-fun papp3 () Int)
(declare-fun GHC.List.span () Int)
(declare-fun GHC.Classes.$62$ () Int)
(declare-fun GHC.Types.False () Bool)
(declare-fun GHC.List.scanr1 () Int)
(declare-fun GHC.Types.$58$ () Int)
(declare-fun GHC.Real.div () Int)
(declare-fun GHC.List.scanl () Int)
(declare-fun GHC.Tuple.$40$$44$$44$$41$ () Int)
(declare-fun papp4 () Int)
(declare-fun GHC.Types.Module () Int)
(declare-fun GHC.List.zip () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792802825$35$$35$d2oN () Int)
(declare-fun GHC.Tuple.$40$$41$ () Int)
(declare-fun GHC.Types.I$35$ () Int)
(declare-fun GHC.List.dropWhile () Int)
(declare-fun autolen () Int)
(declare-fun GHC.Integer.Type.$36$WJn$35$ () Int)
(declare-fun GHC.Real.$94$ () Int)
(declare-fun head () Int)
(declare-fun GHC.Real.mod () Int)
(declare-fun GHC.Real.divMod () Int)
(declare-fun GHC.Integer.Type.Jn$35$ () Int)
(declare-fun GHC.Classes.compare () Int)
(declare-fun papp2 () Int)
(declare-fun GHC.Real.toInteger () Int)
(declare-fun GHC.Real.quotRem () Int)
(declare-fun GHC.Stack.Types.EmptyCallStack () Int)
(declare-fun GHC.List.reverse () Int)
(declare-fun GHC.Integer.Type.$36$WJp$35$ () Int)
(declare-fun Liquid.Test.Assert.$36$trModule () Int)
(declare-fun GHC.List.filter () Int)
(declare-fun fromJust () Int)
(declare-fun GHC.List.cycle () Int)
(declare-fun GHC.List.$33$$33$ () Int)
(declare-fun GHC.List.tail () Int)
(declare-fun papp7 () Int)
(declare-fun GHC.Classes.$47$$61$ () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792802827$35$$35$d2oP () Real)
(declare-fun GHC.List.break () Int)
(declare-fun GHC.Types.True () Bool)
(declare-fun GHC.Types.$91$$93$ () Int)
(declare-fun GHC.List.splitAt () Int)
(declare-fun GHC.Base.$43$$43$ () Int)
(declare-fun GHC.Real.$58$$37$ () Int)
(declare-fun GHC.Tuple.$40$$44$$41$ () Int)
(declare-fun GHC.Real.quot () Int)
(declare-fun GHC.Real.$47$ () Int)
(declare-fun lq_karg$36$VV$35$$35$374$35$$35$k_$35$$35$375 () Int)
(declare-fun GHC.Classes.$38$$38$ () Int)
(declare-fun VV$35$$35$F$35$$35$2 () Real)
(declare-fun GHC.Types.GT () Int)
(declare-fun GHC.Classes.C$58$IP () Int)
(declare-fun GHC.Classes.$124$$124$ () Int)
(declare-fun Data.Either.Left () Int)
(declare-fun GHC.List.last () Int)
(declare-fun GHC.Integer.Type.S$35$ () Int)
(declare-fun GHC.List.scanl1 () Int)
(declare-fun Data.Either.Right () Int)
(declare-fun GHC.Num.$45$ () Int)
(declare-fun len () Int)
(declare-fun papp6 () Int)
(declare-fun GHC.Base.. () Int)
(declare-fun x_Tuple22 () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792802822$35$$35$d2oK () Str)
(declare-fun lq_anf$36$$35$$35$7205759403792802826$35$$35$d2oO () Real)
(declare-fun lq_anf$36$$35$$35$7205759403792802824$35$$35$d2oM () Str)
(declare-fun GHC.Real.$36$W$58$$37$ () Int)
(declare-fun GHC.Real.fromRational () Int)
(declare-fun isJust () Int)
(declare-fun GHC.List.takeWhile () Int)
(declare-fun GHC.Types.TrNameD () Int)
(declare-fun x_Tuple31 () Int)
(declare-fun GHC.Integer.Type.Jp$35$ () Int)
(declare-fun lit$36$liquidhaskell$45$test$45$0.1.0.0$45$inplace () Str)
(declare-fun GHC.IO.Exception.IOError () Int)
(declare-fun GHC.List.take () Int)
(declare-fun GHC.Stack.Types.PushCallStack () Int)
(declare-fun lit$36$Liquid.Test.Assert () Str)
(declare-fun GHC.Classes.$60$$61$ () Int)
(declare-fun GHC.Types.TrNameS () Int)
(declare-fun GHC.Enum.C$58$Bounded () Int)
(declare-fun GHC.Base.map () Int)
(declare-fun VV$35$$35$F$35$$35$3 () Int)
(declare-fun GHC.Base.$36$ () Int)
(declare-fun papp1 () Int)
(declare-fun GHC.Classes.max () Int)
(declare-fun GHC.Classes.$60$ () Int)
(declare-fun tail () Int)
(declare-fun GHC.Stack.Types.FreezeCallStack () Int)
(declare-fun GHC.Num.$42$ () Int)
(declare-fun GHC.Real.recip () Int)
(declare-fun GHC.Maybe.Nothing () Int)
(declare-fun GHC.Types.EQ () Int)
(declare-fun GHC.List.scanr () Int)
(declare-fun GHC.Num.negate () Int)
(declare-fun GHC.Real.fromIntegral () Int)
(declare-fun GHC.Maybe.Just () Int)
(declare-fun GHC.Classes.min () Int)
(declare-fun GHC.List.head () Int)
(declare-fun x_Tuple32 () Int)
(declare-fun GHC.List.repeat () Int)
(declare-fun GHC.Classes.not () Int)
(declare-fun GHC.Num.$43$ () Int)
(declare-fun Data.Tuple.fst () Int)
(declare-fun GHC.Float.$36$fFractionalFloat () Int)
(declare-fun GHC.Err.error () Int)
(declare-fun snd () Int)
(declare-fun fst () Int)
(declare-fun Data.Tuple.snd () Int)
(declare-fun lq_anf$36$$35$$35$7205759403792802823$35$$35$d2oL () Int)
(declare-fun apply$35$$35$21 (Int (_ BitVec 32)) Bool)
(declare-fun apply$35$$35$16 (Int Str) Bool)
(declare-fun apply$35$$35$8 (Int Bool) Str)
(declare-fun apply$35$$35$19 (Int Str) (_ BitVec 32))
(declare-fun apply$35$$35$12 (Int Real) Real)
(declare-fun apply$35$$35$24 (Int (_ BitVec 32)) (_ BitVec 32))
(declare-fun apply$35$$35$0 (Int Int) Int)
(declare-fun apply$35$$35$7 (Int Bool) Real)
(declare-fun apply$35$$35$15 (Int Str) Int)
(declare-fun apply$35$$35$1 (Int Int) Bool)
(declare-fun apply$35$$35$13 (Int Real) Str)
(declare-fun apply$35$$35$14 (Int Real) (_ BitVec 32))
(declare-fun apply$35$$35$22 (Int (_ BitVec 32)) Real)
(declare-fun apply$35$$35$9 (Int Bool) (_ BitVec 32))
(declare-fun apply$35$$35$2 (Int Int) Real)
(declare-fun apply$35$$35$10 (Int Real) Int)
(declare-fun apply$35$$35$23 (Int (_ BitVec 32)) Str)
(declare-fun apply$35$$35$18 (Int Str) Str)
(declare-fun apply$35$$35$6 (Int Bool) Bool)
(declare-fun apply$35$$35$11 (Int Real) Bool)
(declare-fun apply$35$$35$3 (Int Int) Str)
(declare-fun apply$35$$35$20 (Int (_ BitVec 32)) Int)
(declare-fun apply$35$$35$4 (Int Int) (_ BitVec 32))
(declare-fun apply$35$$35$5 (Int Bool) Int)
(declare-fun apply$35$$35$17 (Int Str) Real)
(declare-fun coerce$35$$35$21 ((_ BitVec 32)) Bool)
(declare-fun coerce$35$$35$16 (Str) Bool)
(declare-fun coerce$35$$35$8 (Bool) Str)
(declare-fun coerce$35$$35$19 (Str) (_ BitVec 32))
(declare-fun coerce$35$$35$12 (Real) Real)
(declare-fun coerce$35$$35$24 ((_ BitVec 32)) (_ BitVec 32))
(declare-fun coerce$35$$35$0 (Int) Int)
(declare-fun coerce$35$$35$7 (Bool) Real)
(declare-fun coerce$35$$35$15 (Str) Int)
(declare-fun coerce$35$$35$1 (Int) Bool)
(declare-fun coerce$35$$35$13 (Real) Str)
(declare-fun coerce$35$$35$14 (Real) (_ BitVec 32))
(declare-fun coerce$35$$35$22 ((_ BitVec 32)) Real)
(declare-fun coerce$35$$35$9 (Bool) (_ BitVec 32))
(declare-fun coerce$35$$35$2 (Int) Real)
(declare-fun coerce$35$$35$10 (Real) Int)
(declare-fun coerce$35$$35$23 ((_ BitVec 32)) Str)
(declare-fun coerce$35$$35$18 (Str) Str)
(declare-fun coerce$35$$35$6 (Bool) Bool)
(declare-fun coerce$35$$35$11 (Real) Bool)
(declare-fun coerce$35$$35$3 (Int) Str)
(declare-fun coerce$35$$35$20 ((_ BitVec 32)) Int)
(declare-fun coerce$35$$35$4 (Int) (_ BitVec 32))
(declare-fun coerce$35$$35$5 (Bool) Int)
(declare-fun coerce$35$$35$17 (Str) Real)
(declare-fun smt_lambda$35$$35$21 ((_ BitVec 32) Bool) Int)
(declare-fun smt_lambda$35$$35$16 (Str Bool) Int)
(declare-fun smt_lambda$35$$35$8 (Bool Str) Int)
(declare-fun smt_lambda$35$$35$19 (Str (_ BitVec 32)) Int)
(declare-fun smt_lambda$35$$35$12 (Real Real) Int)
(declare-fun smt_lambda$35$$35$24 ((_ BitVec 32) (_ BitVec 32)) Int)
(declare-fun smt_lambda$35$$35$0 (Int Int) Int)
(declare-fun smt_lambda$35$$35$7 (Bool Real) Int)
(declare-fun smt_lambda$35$$35$15 (Str Int) Int)
(declare-fun smt_lambda$35$$35$1 (Int Bool) Int)
(declare-fun smt_lambda$35$$35$13 (Real Str) Int)
(declare-fun smt_lambda$35$$35$14 (Real (_ BitVec 32)) Int)
(declare-fun smt_lambda$35$$35$22 ((_ BitVec 32) Real) Int)
(declare-fun smt_lambda$35$$35$9 (Bool (_ BitVec 32)) Int)
(declare-fun smt_lambda$35$$35$2 (Int Real) Int)
(declare-fun smt_lambda$35$$35$10 (Real Int) Int)
(declare-fun smt_lambda$35$$35$23 ((_ BitVec 32) Str) Int)
(declare-fun smt_lambda$35$$35$18 (Str Str) Int)
(declare-fun smt_lambda$35$$35$6 (Bool Bool) Int)
(declare-fun smt_lambda$35$$35$11 (Real Bool) Int)
(declare-fun smt_lambda$35$$35$3 (Int Str) Int)
(declare-fun smt_lambda$35$$35$20 ((_ BitVec 32) Int) Int)
(declare-fun smt_lambda$35$$35$4 (Int (_ BitVec 32)) Int)
(declare-fun smt_lambda$35$$35$5 (Bool Int) Int)
(declare-fun smt_lambda$35$$35$17 (Str Real) Int)
(declare-fun lam_arg$35$$35$1$35$$35$0 () Int)
(declare-fun lam_arg$35$$35$2$35$$35$0 () Int)
(declare-fun lam_arg$35$$35$3$35$$35$0 () Int)
(declare-fun lam_arg$35$$35$4$35$$35$0 () Int)
(declare-fun lam_arg$35$$35$5$35$$35$0 () Int)
(declare-fun lam_arg$35$$35$6$35$$35$0 () Int)
(declare-fun lam_arg$35$$35$7$35$$35$0 () Int)
(declare-fun lam_arg$35$$35$1$35$$35$15 () Str)
(declare-fun lam_arg$35$$35$2$35$$35$15 () Str)
(declare-fun lam_arg$35$$35$3$35$$35$15 () Str)
(declare-fun lam_arg$35$$35$4$35$$35$15 () Str)
(declare-fun lam_arg$35$$35$5$35$$35$15 () Str)
(declare-fun lam_arg$35$$35$6$35$$35$15 () Str)
(declare-fun lam_arg$35$$35$7$35$$35$15 () Str)
(declare-fun lam_arg$35$$35$1$35$$35$10 () Real)
(declare-fun lam_arg$35$$35$2$35$$35$10 () Real)
(declare-fun lam_arg$35$$35$3$35$$35$10 () Real)
(declare-fun lam_arg$35$$35$4$35$$35$10 () Real)
(declare-fun lam_arg$35$$35$5$35$$35$10 () Real)
(declare-fun lam_arg$35$$35$6$35$$35$10 () Real)
(declare-fun lam_arg$35$$35$7$35$$35$10 () Real)
(declare-fun lam_arg$35$$35$1$35$$35$20 () (_ BitVec 32))
(declare-fun lam_arg$35$$35$2$35$$35$20 () (_ BitVec 32))
(declare-fun lam_arg$35$$35$3$35$$35$20 () (_ BitVec 32))
(declare-fun lam_arg$35$$35$4$35$$35$20 () (_ BitVec 32))
(declare-fun lam_arg$35$$35$5$35$$35$20 () (_ BitVec 32))
(declare-fun lam_arg$35$$35$6$35$$35$20 () (_ BitVec 32))
(declare-fun lam_arg$35$$35$7$35$$35$20 () (_ BitVec 32))
(declare-fun lam_arg$35$$35$1$35$$35$5 () Bool)
(declare-fun lam_arg$35$$35$2$35$$35$5 () Bool)
(declare-fun lam_arg$35$$35$3$35$$35$5 () Bool)
(declare-fun lam_arg$35$$35$4$35$$35$5 () Bool)
(declare-fun lam_arg$35$$35$5$35$$35$5 () Bool)
(declare-fun lam_arg$35$$35$6$35$$35$5 () Bool)
(declare-fun lam_arg$35$$35$7$35$$35$5 () Bool)
(assert (distinct lit$36$Liquid.Test.Assert lit$36$liquidhaskell$45$test$45$0.1.0.0$45$inplace))
(assert (distinct GHC.Types.True GHC.Types.False))
(assert (distinct GHC.Types.EQ GHC.Types.GT GHC.Types.LT))
(assert (= (strLen lit$36$liquidhaskell$45$test$45$0.1.0.0$45$inplace) 34))
(assert (= (strLen lit$36$Liquid.Test.Assert) 18))
(push 1)
(assert (and GHC.Types.True (= lq_anf$36$$35$$35$7205759403792802822$35$$35$d2oK lit$36$liquidhaskell$45$test$45$0.1.0.0$45$inplace) (= lq_anf$36$$35$$35$7205759403792802824$35$$35$d2oM lit$36$Liquid.Test.Assert) (not GHC.Types.False)))
(push 1)
(assert (not (= 0 1)))
(check-sat)
; SMT Says: Sat
(pop 1)
(pop 1)
(push 1)
(assert (and GHC.Types.True (= lq_anf$36$$35$$35$7205759403792802826$35$$35$d2oO 1.00000) (= lq_anf$36$$35$$35$7205759403792802827$35$$35$d2oP 1.00000e9) (and (= VV$35$$35$F$35$$35$2 1.00000e9) (= VV$35$$35$F$35$$35$2 lq_anf$36$$35$$35$7205759403792802827$35$$35$d2oP)) (not GHC.Types.False)))
(push 1)
(assert (not (not (= VV$35$$35$F$35$$35$2 0))))
(check-sat)
; SMT Says: Error "line 286 column 150: unknown constant e9"
(pop 1)
(pop 1)
—
You are receiving this because you commented.
Reply to this email directly, view it on GitHub
<https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/issues/1762*issuecomment-737917956__;Iw!!Mih3wA!Wj3YAU1WVGVo-UMl1meMIjFpEMNlPfD7CK5b0KZAcw1UFWkiPX_Kaw1n0d49RKmZ$>,
or unsubscribe
<https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OBOZVG2YD464GBCEYTSS575TANCNFSM4RVGIFRQ__;!!Mih3wA!Wj3YAU1WVGVo-UMl1meMIjFpEMNlPfD7CK5b0KZAcw1UFWkiPX_Kaw1n0dc3iJYA$>
.
|
|
I was able to get Liquid Haskell to successfully analyze my project. In addition to what was stated above. I had to remove the Storable Instance via CPP and use the following ghc-options: -fplugin=LiquidHaskell -fplugin-opt=LiquidHaskell:--fast -fplugin-opt=LiquidHaskell:--max-case-expand=0 -fplugin-opt=LiquidHaskell:--no-termination |
|
Wow, that's great, thanks for letting us know Nathan!
…On Fri, Jan 29, 2021 at 8:58 AM Nathan Waivio ***@***.***> wrote:
I was able to get Liquid Haskell to successfully analyze my project. In
addition to what was stated above. I had to remove the Storable Instance
via CPP and use the following ghc-options: -fplugin=LiquidHaskell
-fplugin-opt=LiquidHaskell:--fast
-fplugin-opt=LiquidHaskell:--max-case-expand=0
-fplugin-opt=LiquidHaskell:--no-termination
—
You are receiving this because you commented.
Reply to this email directly, view it on GitHub
<https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/issues/1762*issuecomment-769924939__;Iw!!Mih3wA!SrOqAlgUuh_ZJU0Mm80HK_iN8NfCr2jWX6sW_V3WGggIMv4SFDaW58-LCyXEnmR0$>,
or unsubscribe
<https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OBL2RSJYU7DEY3DP63S4LSLNANCNFSM4RVGIFRQ__;!!Mih3wA!SrOqAlgUuh_ZJU0Mm80HK_iN8NfCr2jWX6sW_V3WGggIMv4SFDaW58-LCxPIvlfl$>
.
|
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
My whole goal is to verify that some my usage of sqrt could be confirmed to be within the domain of the function like: {-@ sqrt :: {v:Double | 0 <= v} -> Double @-} holds in my library so that I can have confidence that NaN will not happen. I haven't gotten to that part yet and am still trying to enable LiquidHaskell and get it to build with my library.
Issue#1
I'm getting a GHC error for the Safe Haskell Language extension, probably due to the re-export of Base. I worked around this issue by #ifdef'ing {-# LANGUAGE Safe #-} out when Liquid Haskell is being used.
Issue#2
I'm getting a Stack Overflow. I worked around this by disabling derived instances. I also tried the suggested {-@ LIQUID --max-case-expand=0 @-} with no perceived benefit and tried changing the RTS to max out the Stack size, with no effect.
Issue#3
I get a crash I believe due to a constant used in my code of 128*eps = 1.4210854715202004e-14, I have not been able to work around this issue.
To be fair GHC has had some issues with compiling my library as well. The branch in my repo that generates the unknown constant error is here: https://github.com/waivio/cl3/tree/liquid
Are these known issues? Is what I'm trying to do not supported?
The text was updated successfully, but these errors were encountered: