search

ucsd-progsys / liquidhaskell

Liquid Types For Haskell
BSD 3-Clause "New" or "Revised" License
1.18k stars 133 forks source link

Question: Disable default Specs? #1489

Open googleson78 opened 5 years ago

googleson78 commented 5 years ago

Is there any way to disable/override the usage of the default spec files that are automatically included (from the include folder in this repo), other than recompiling without them?

ranjitjhala commented 5 years ago

Do you mean for particular functions? Or do you mean for an entire module?

On Fri, May 10, 2019 at 2:07 PM Georgi Lyubenov notifications@github.com wrote:

Is there any way to disable/override the usage of the default spec files that are automatically included (from the include folder in this repo), other than recompiling without them?

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1489, or mute the thread https://github.com/notifications/unsubscribe-auth/AAMS4OF5K6M6WGHI74GJMYDPUXPY3ANCNFSM4HMGHL2Q .

googleson78 commented 5 years ago

I know you can disable checks on a function with a {-@ ignore @-} pragma but I was thinking about something more like Haskell's {-# Language NoImplicitPrelude #-}, disabling "prelude" entirely. Or for example overriding include/Data/ByteString.spec from this repo with my own ByteString.spec

ranjitjhala commented 5 years ago

Hmm no way to do that unfortunately. Could be an easy to add feature though...

On Fri, May 10, 2019 at 2:32 PM Georgi Lyubenov notifications@github.com wrote:

I know you can disable checks on a function with a {-@ ignore @-} pragma but I was thinking about something more like Haskell's {-# Language NoImplicitPrelude #-}, disabling "prelude" entirely. Or for example overriding include/Data/ByteString.spec from this repo with my own ByteString.spec

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1489#issuecomment-491436366, or mute the thread https://github.com/notifications/unsubscribe-auth/AAMS4OFKQPV3IWDHP2SCFKDPUXSVJANCNFSM4HMGHL2Q .

googleson78 commented 5 years ago

Which files in include are "mandatory" for liquid to work? (I would be happy to read documentation on this if there is any)

Removing include entirely from idirs in mkOpts breaks liquid -

LH.Bare.listTyDataCons:0:0: Error: Illegal data refinement for `[]`
     Size function len x should have type int.
     Unbound symbol len --- perhaps you meant: head, x ?
ranjitjhala commented 5 years ago

Good question! I think The ones that are “transitively imported” from Prelude.spec

On Fri, May 17, 2019 at 2:23 PM Georgi Lyubenov notifications@github.com wrote:

Which files in include are "mandatory" for liquid to work? (I would be happy to read documentation on this if there is any)

Removing include entirely from idirs in mkOpts breaks liquid -

LH.Bare.listTyDataCons:0:0: Error: Illegal data refinement for [] Size function len x should have type int. Unbound symbol len --- perhaps you meant: head, x ?

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://github.com/ucsd-progsys/liquidhaskell/issues/1489?email_source=notifications&email_token=AAMS4OHV3Y7LNW6LDDUJ6STPV4O5DA5CNFSM4HMGHL22YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGODVV4VZI#issuecomment-493603557, or mute the thread https://github.com/notifications/unsubscribe-auth/AAMS4OEF2XZMTIEU2VNDG4DPV4O5DANCNFSM4HMGHL2Q .

googleson78 commented 5 years ago

I can't figure out an easy way to exclude the default specs then (without hard-coding paths to specific files, which is a bad idea imo).

facundominguez commented 3 months ago

At the moment it is possible to exclude specs coming from some particular package --exclude-automatic-assumptions-for=PACKAGE. But excluding specs from the liquidhaskell module would likely exclude too much.

A similar mechanism could be implemented per module or perhaps per binding. But before implementing something like that it would be necessary to understand the use case.

For instance, I'm thinking of some mechanism to label specs or predicates, and then selectively enable those specs with a flag that refers to the labels. My use case would be splitting all the checks that Liquid Haskell does so the user can select only the ones she is interested in. In that way, if we want to validate the schema of a database query, we don't need to make LH happy about partial functions on lists or pointer arithmetic as well.

googleson78 commented 3 months ago

In that way, if we want to validate the schema of a database query, we don't need to make LH happy about partial functions on lists or pointer arithmetic as well.

This was my initial motivation as well - I didn't want to deal with the proofs that the pointer operations required of me.