Working with Spec Files

[Jack Wrenn]

I've filed a bug report for this, but I think I'm perhaps just making a mistake and someone might be able to point me in the right direction.

Here's the scenario:

I have some library file, toyprogram/Library.hs, that I do not want to verify:

module Library (foo) where
foo a = a

I have a spec for Library, toyprogram/Library.spec, that has a time-bomb refinement (so we'll know if it's used):

module Library where
foo :: a:{v:t | false} -> t

And I have a client file, toyprogram/Client.hs, that I would like to verify using LiquidHaskell:

module Client where
import Library
bar = foo 1

If I run

liquid --idirs=toyprogram/ toyprogram/Client.hs

what I would expect to happen is that LiquidHaskell report UNSAFE, since I expect that LiquidHaskell will use the flawed Library.spec to refine foo.

However, that command is reporting SAFE for me. LiquidHaskell is reporting SAFE even if Library.spec has syntax errors. It seems like Library.spec is being ignored. How can I point LiquidHaskell towards my spec files?

Best,

Jack

[Niki Vazou]

Is there a reason why you want to use the spec file? You can write local assumed signatures in your Client file, i.e.

module Client where
import Library

{-@ assume foo :: a:{v:t | false} -> t @-}

bar = foo 1

--
You received this message because you are subscribed to the Google Groups "liquidhaskell" group.
To unsubscribe from this group and stop receiving emails from it, send an email to liquidhaskel...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--

Niki Vazou

[Jack Wrenn]

Thanks for the swift reply! That's how I've been developing my specs up until now, but I'm trying to integrate them into a code-generation pipeline that doesn't support comments. If I cannot point LiquidHaskell towards a specfile, my backup plan is sed'ing them into the generated file.

Best,

Jack

[Niki Vazou]

Not exactly sure what is going on with the spec files, I suspect there is a bug, but will look into that. 

Instead, if you want to specify LiquidHaskell types without comments you can use our new (ie beta) feature, quasiquotations:

https://github.com/ucsd-progsys/liquidhaskell/tree/develop#modules-with-code-quasiquotation