Liquid-Dev-Mode prototype #1706
Conversation
|
Tried this with |
|
Super minor point @adinapoli -- can you also add the above text to the document for how to generate |
Good point, although I am wondering whether or not that document would be the right place for it. What about another |
|
I think the most important aspect here is that the documentation on how to use the dev mode does not remain hidden in the description of this PR. The second most important aspect is discoverability. So creating a new file is fine from my perspective. But ideally, already place a link to it from somewhere (or even several places), so that it can be found. |
|
👍 both these are things that I (and Niki and other potential LH developers
- as opposed to users - need to know, hence ultimately I would like them to
be gathered as such)
…On Thu, Jul 16, 2020 at 12:20 AM Andres Löh ***@***.***> wrote:
I think the most important aspect here is that the documentation on how to
use the dev mode does not remain hidden in the description of this PR. The
second most important aspect is discoverability. So creating a new file is
fine from my perspective. But ideally, already place a link to it from
somewhere (or even several places), so that it can be found.
—
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/pull/1706*issuecomment-659210849__;Iw!!Mih3wA!TRebqBgWY6YJV35Z7rl6ILEkAw9gjKJQ7-3q6ReitnjBNruALdHLQ84QTBzRxTR1$>,
or unsubscribe
<https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OCRF6W2O2NL7TVQSADR32S45ANCNFSM4OZTP4CA__;!!Mih3wA!TRebqBgWY6YJV35Z7rl6ILEkAw9gjKJQ7-3q6ReitnjBNruALdHLQ84QTIKyvRBm$>
.
|
This commit factors out the content of the custom 'Setup.hs', which was the same for each and every module into a liquidhaskell module we can then reuse by using the 'setup-depends' directive.
|
@ranjitjhala @kosmikus Ok, I have added a documentation section in the "new" documentation that Ranjit is working on, as part of the "Developers' guide" inside As I was at it, I have factored the content of each and every |
This PR has to be intended as a prototype and can be easily improved. To name something suboptimal, the current
Setup.hsis the same for each package and is duplicated everywhere. Also, the actual value of theLIQUID_DEV_MODEenv var is not taken into account, but maybe it's nice if users could toggle dev mode by passingLIQUID_DEV_MODE=trueandLIQUID_DEV_MODE=false.This PR is a first attempt in speeding up the LiquidHaskell development experience when using the new GHC plugin. The main idea takes inspiration from the stages of a compiler (think GHC) where usually we build a "stage0" compiler to be used to compile the stage1. Similarly we introduce, for each of the
liquid-*packages, a customSetup.hsmodule that disables building the target modules if theLIQUID_DEV_MODEenv var is set.Usage and recommended workflow
This is how one would use this:
To begin with, perform a full build of all the libraries, by doing either
cabal v2-buildorstack build, without specifying any extra environment variables from the command line. This is morally equivalent to our "stage 0".At this point, the content of the
liquid-*packages is considered "trusted" and "frozen", until we don't force another full, non dev build;In order to quickly test changes to the
liquidhaskelllibrary without recompiling theliquid-*packages, we user need to build by passing theLIQUID_DEV_MODEenv var as part of the build command. Examples:Stack
Cabal
It's also possible (but not recommended) to add
LIQUID_DEV_MODEto.bashrcor similar,but this would permanently disable building theliquid-*packages, and this might silently mask breaking changes to the liquidhaskell library that would manifest only when compiling these other packages.LIQUID_DEV_MODE.