Source plugin for LiquidHaskell #1683
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This PR creates a 'GHC.Plugin' module hierarchy in the codebase which will set the stage for the plugin work. Some provisional code is provided that sets up the plugin architecture, without calling into any meaningful LH functions.
This commit uses an IORef to thread (immutable) state around, so that things discovered in the typechecking phase are available at the core pass during plugin compilation.
This commit makes possible to serialise and deserialise BareSpecs from/to interface files.
This commit introduces an experiment GhcMonadLike typeclass which is virtually isomorphic to the 'GhcMonad' class but it doesn't require an instance for 'ExceptionMonad', allowing us to call most of the functions present in 'GHC.Interface' also in 'CoreM'.
This commit removes the need of calling `updLiftedSpec` from the plugin, because we don't need access to serialised specs on disk.
This commit reverses the position of the spec comments we receive from the parseHook in the Plugin. This was necessary for some tests to pass as it seems LiquidHaskell relies on the spec annotations to arrive in a particular order.
The key for efficiently loading specs from disk lies in making the SpecEnv type a bit more sophisticated. This commit tries to do that in an experimental fashion.
This commit separates out some general-utility Haskell files pre-shipped as part of the `include` directory as a standalone `liquid-prelude` package so that they can be compiled using the plugin.
This commit reuses the two functions 'qualifiedImports' and 'allImports' from the GHC.Interface module, trying to reduce the gap between this module and the implementation at GHC.Plugin.
This commit passes the '-w' flag to suppress all the warnings we would otherwise get when compiling the 'text' and 'bytestring' benchmarks, which would make the test failure dump a lot of output, making debugging harder.
This commit imports the `Data.ByteString.Lazy.Internal` module inside `Data.Text.Encoding.Fusion` and then adds the `--prune-unsorted` and `--compilespec` Liquid pragmas to fix the last remaining tests. It also re-enables `.Fusion` tests so that they would still pass for the old executable.
adinapoli
force-pushed
the
adinapoli/source-plugin
branch
from
81b298e
to
e20d987
Compare
|
Thanks @adinapoli!! I've been arguing for ages that LiquidHaskell should be a GHC plugin but don't have the time anymore to do the work. |
adinapoli
force-pushed
the
adinapoli/source-plugin
branch
from
f360735
to
e772ecd
Compare
This commit adds a new field to the LH's `Config` data structure, unsurprisingly-named `loggingVerbosity`, which allows LH to have a better control over the granularity of logging. This allows the source plugin to run in `Quiet` mode (which is now the default) but the executable to be customised to run by default using the `--normal` mode, to show things like the progress bar.
adinapoli
force-pushed
the
adinapoli/source-plugin
branch
6 times, most recently
from
fca08c4
to
963cbd2
Compare
adinapoli
force-pushed
the
adinapoli/source-plugin
branch
from
963cbd2
to
eaf8a5c
Compare
This commit re-exports the source plugin under the 'LiquidHaskell' module, so that users can simply use `-fplugin=LiquidHaskell`.
nikivazou
approved these changes
Jun 9, 2020
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR is the "MVP" (Minimum Viable Product) that allows LiquidHaskell to be used as a compiler plugin and integrated as part of the GHC compilation pipeline. It requires the companion
liquid-fixpointPR, see ucsd-progsys/liquid-fixpoint#435.While this PR could be merged as-it-is, I will try documenting below what is outstanding in terms of "bells & whistles". None of what's below (with the notable exception of the CI failure) should stop merging this.
Ergonomic adjustments
As said previously, we currently have the plugin living at
Language.Haskell.Liquid.GHC.Plugin, which makes perfect sense in terms of our internal module hierarchy but it's a bit of a mouthful for users. We should probably have just aLiquidHaskellmodule which re-exports the plugin, so that users can use it just by having-fplugin=LiquidHaskellin their cabal files. I will try adding this as extra comments to this PR.Documentation
I have added some basic documentation but more polishing is needed, but that can come after merging this initial strand of work. In particular, I have tried to revamp the current
READMEto make people aware of the new plugin and the migration path, but you might want to further expand on that.CI
While CircleCI is happily passing, AppVeyor seems to be struggling, with a failure similar to the one described here but none of the proposed fixes actually work. I have seen this in the past while working on the plugin and I band-aided that by adding
-fexternal-interpreterwhen building the library. Recently, however, it seems likeliquid-ghc-primis failing to build:It's not really clear to me if this is a stack-specific issue or just a misconfigured build configuration. I will try playing with it, although the feedback cycle is a bit slow as I can't test this locally (I am on Mac OS X and I don't have a Windows VM lying around).
Migration plan
Currently I had to leave the "hardcoded prelude" files, living inside the
includedirectory, so that the old executable could work just fine. Having said that, we should lay out a migration plan where we phase out the legacy executable and we clean up the the codebase from all these redundant files.Liquid-platform packages
Currently, I have done my best to move virtually all the files from
includeinto theirliquid-*mirror package counterparts. Having said that, there are still packages which haven't been fully tested or completed (for exampleliquid-bytestring) so we might want to spend a bit of time there. Last but not least we should probably move away from the "mega-repo" approach as we are doing now but rather have the differentliquid-*projects into separate repository. I think this will help with versioning and revisioning.