Merge pull request #1353 from ucsd-progsys/phadej-ghc-8.4

Phadej ghc 8.4

Author: ranjitjhala

.circleci/config.yml

@@ -4,7 +4,7 @@ version: 2.0
 jobs:
   build:
     docker:
-      - image: fpco/stack-build:lts-10.0
+      - image: fpco/stack-build:lts-12.2
     steps:
       - add_ssh_keys
       - run: apt-get install z3
@@ -31,13 +31,16 @@ jobs:
           name: Test
           command: |
             stack clean
-            mkdir -p $CIRCLE_TEST_REPORTS/junit
-            stack test liquidhaskell:test --flag liquidhaskell:include --flag liquidhaskell:devel --test-arguments="-t 1200s -j2 --xml=$CIRCLE_TEST_REPORTS/junit/main-test-results.xml": #--liquid-opts='--cores=1'":
-            stack test liquidhaskell:liquidhaskell-parser --test-arguments="-j2 --xml=$CIRCLE_TEST_REPORTS/junit/parser-test-results.xml":
+            mkdir -p /tmp/junit
+            stack test liquidhaskell:test --flag liquidhaskell:include --flag liquidhaskell:devel --test-arguments="-t 1200s --xml=/tmp/junit/main-test-results.xml": #--liquid-opts='--cores=1'":
+            stack test liquidhaskell:liquidhaskell-parser --test-arguments="--xml=/tmp/junit/parser-test-results.xml":
             stack sdist
-            stack haddock liquidhaskell --flag liquidhaskell:-devel --no-haddock-deps --haddock-arguments="--no-print-missing-docs --odir=$CIRCLE_ARTIFACTS"
-            mkdir -p $CIRCLE_TEST_REPORTS/tasty
-            cp -r tests/logs/cur $CIRCLE_TEST_REPORTS/tasty/log
+            # stack haddock liquidhaskell --flag liquidhaskell:-devel --no-haddock-deps --haddock-arguments="--no-print-missing-docs --odir=$CIRCLE_ARTIFACTS"
+            stack haddock liquidhaskell  --no-haddock-deps --haddock-arguments="--no-print-missing-docs"
+      - store_test_results:
+          path: /tmp/junit
+      - store_artifacts:
+          path: tests/logs/cur
       - run:
           name: Dist
           command: stack sdist

CHANGES.md

@@ -2,6 +2,10 @@
 
 ## NEXT 
 
+## 0.8.4.0 
+
+- Support for GHC 8.4.3 
+
 ## 0.8.2.2
 
 - Support for GHC 8.2.2 

FAILING_TESTS.txt

@@ -110,5 +110,3 @@ tags:
 	# hasktags -c src/
 	# hasktags -e src/
 
-ghcid:
-	ghcid --command "stack ghci --main-is liquidhaskell:exe:liquid"

Makefile

@@ -58,36 +58,35 @@ See [this file](NIX.md) for instructions on running inside a custom `nix`-shell.
 How To Run Regression Tests
 ---------------------------
 
+You can run all the tests by
+
     $ stack test
 
-To use threads to speed up the tests
+To pass in specific parameters and run a subset of the tests 
 
-    $ make THREADS=30 test
+    $ stack test liquidhaskell --fast  --test-arguments "--liquid-opts --no-termination -p Unit"
 
 Or your favorite number of threads, depending on cores etc.
 
 You can directly extend and run the tests by modifying
 
     tests/test.hs
 
-To run the regression test *and* the benchmarks run
-
-    $ make all-test
-
 How to Profile
 --------------
 
 1. Build with profiling on
 
     ```
-    $ make pdeps && make prof
+    $ stack build liquidhaskell --fast --profile
     ```
 
+
 2. Run with profiling
 
     ```
-    $ time liquid range.hs +RTS -hc -p
-    $ time liquid range.hs +RTS -hy -p
+    $ stack exec -- liquid range.hs +RTS -hc -p
+    $ stack exec -- liquid range.hs +RTS -hy -p
     ```
 
     Followed by this which shows the stats file
@@ -111,7 +110,7 @@ How to Get Stack Traces On Exceptions
 1. Build with profiling on
 
     ```
-    $ make pdeps && make prof
+    $ stack build liquidhaskell --fast --profile
     ```
 
 2. Run with backtraces
@@ -120,6 +119,10 @@ How to Get Stack Traces On Exceptions
     $ liquid +RTS -xc -RTS foo.hs
     ```
 
+    ```
+    stack exec -- liquid List00.hs +RTS -p -xc -RTS
+    ```
+
 Working With Submodules
 -----------------------
 
@@ -1464,3 +1467,36 @@ Suppose that the current version of Liquid Haskell is `A.B.C.D`:
 
 + The `A` component shall be updated at the sole discretion of the project owners.
 
+Updating GHC
+============
+
+Here's a script to generate the diff for the `desugar` modules.
+
+```
+export GHCSRC=$HOME/Documents/ghc
+
+# Checkout GHC-8.2.2
+(cd $GHCSRC && git checkout ghc-8.2.2 && git pull)
+
+# make a patch
+diff -ur $GHCSRC/compiler/deSugar src/Language/Haskell/Liquid/Desugar > liquid.patch
+
+# Checkout GHC-8.4.3
+(cd $GHCSRC && git checkout ghc-8.2.2 && git pull)
+
+# Copy GHC desugarer to temporary directory
+cp -r $GHCSRC/compiler/deSugar .
+
+# Patch
+(cd deSugar && patch -p5 --merge --ignore-whitespace < ../liquid.patch)
+
+# Copy stuff over
+for i in src/Language/Haskell/Liquid/Desugar/*.*; do j=$(basename $i); echo $j; cp deSugar/$j src/Language/Haskell/Liquid/Desugar; done
+```
+
+
+Here's the magic diff that we did at some point that we keep bumping up to new GHC versions:
+
+https://github.com/ucsd-progsys/liquidhaskell/commit/d380018850297b8f1878c33d0e4c586a1fddc2b8#diff-3644b76a8e6b3405f5492d8194da3874R224 
+
+

README.md

@@ -1,4 +1,15 @@
-### CallStack/Error
+# TODO
+
+- [] Fix termination tests in fail.txt 
+- [] Fix resolve     tests in fail.txt 
+- [] Fix eq-repr     tests in fail.txt 
+- [] Remove trace 
+- [] Remove warnings 
+- [] fix circle
+- [] merge PR
+
+
+## CallStack/Error
 
 The use of `Prelude.error` gives a crazy performance hit
 apparently even without cutvars being generated, this is
@@ -33,10 +44,6 @@ TODO
 Prune Unsorted Refs
 -------------------
 
-* mergeDataConTypes
-* makeMeasureSpec'
-* meetDataConSpec
-
 The below gives a nice SORT error
 
 ```haskell
@@ -1237,3 +1244,4 @@ GHC 7.10
 
 - termination metrics are required in a few places where they were not previously
   - my guess is that ghc's behaviour for grouping functions in a `Rec` binder have changed
+

TODO.md

@@ -468,11 +468,11 @@ pack str = unsafeCreate (P.length str) $ \p -> go p str
 
 #else /* hack away */
 
-pack str = unsafeCreate (P.length str) $ \(Ptr p) -> stToIO (go p 0# str)
+pack str = unsafeCreate (P.length str) $ \(Ptr p) -> stToIO (goz str p 0# )
     where
-        {-@ decrease go 3 @-}
-        go _ _ []        = return ()
-        go p i (W8# c:cs) = writeByte p i c >> go p (i +# 1#) cs
+        {- goz :: _ -> _ -> cs:_ -> _ / [len cs] -}
+        goz []         _ _  = return ()
+        goz (W8# c:cs) p i  = writeByte p i c >> goz cs p (i +# 1#) 
 
         writeByte p i c = ST $ \s# ->
             case writeWord8OffAddr# p i c s# of s2# -> (# s2#, () #)
@@ -2343,3 +2343,38 @@ findFromEndUntil f ps@(PS x s l) =
          else findFromEndUntil f (PS x s (l-1))
 
 
+
+-- // for unfoldrN 
+{-@ qualif PLenNat(v:GHC.Ptr.Ptr a): (0 <= plen v) 
+  @-}
+
+-- // for UnpackFoldrINLINED
+{-@ qualif UnpackFoldrINLINED(v:List a, n:int, acc:List a): (len v = n + 1 + (len acc))
+  @-}
+
+-- // for ByteString.inits
+{-@ qualif BLenGt(v:Data.ByteString.Internal.ByteString, n:int): ((bLength v) > n)
+  @-}
+
+-- // for ByteString.concat
+{-@ qualif BLens(v:List Data.ByteString.Internal.ByteString) : (0 <= bLengths v)
+  @-}
+
+{-@ qualif BLenLE(v:GHC.Ptr.Ptr a, bs:List Data.ByteString.Internal.ByteString): (bLengths bs <= plen v) 
+  @-}
+
+-- // for ByteString.splitWith
+{-@ qualif SplitWith(v:List Data.ByteString.Internal.ByteString, l:int): ((bLengths v) + (len v) - 1 = l)
+  @-}
+
+-- // for ByteString.unfoldrN
+{-@ qualif PtrDiff(v:int, i:int, p:GHC.Ptr.Ptr a): (i - v <= plen p)
+  @-}
+
+-- // for ByteString.split
+{-@ qualif BSValidOff(v:int,l:int,p:GHC.ForeignPtr.ForeignPtr a): (v + l <= fplen p) 
+  @-}
+
+
+{-@ qualif SplitLoop(v:List Data.ByteString.Internal.ByteString, l:int, n:int): ((bLengths v) + (len v) - 1 = l - n)
+  @-}