Merge pull request #2494 from ucsd-progsys/fd/simplify-fqout

Update liquid-fixpoint to include simplification of fqout files
ucsd-progsys · Mar 10, 2025 · 1d133ad · 1d133ad
2 parents 152ecbf + 4bff2cb
commit 1d133ad
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 6 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -2,6 +2,8 @@
 
 ## Next
 
+- Simplify kvar solutions in fqout files [liquid-fixpoint#741](https://github.com/ucsd-progsys/liquid-fixpoint/pull/741).
+
 ## 0.9.10.1.2 (2025-03-06)
 
 - Implement opaque reflection, a feature to allow reflecting functions which

diff --git a/liquid-fixpoint b/liquid-fixpoint
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs
@@ -219,14 +219,11 @@ lhDynFlags _ hscEnv =
 --------------------------------------------------------------------------------
 
 -- | LiquidHaskell requires the desugarer to keep source note ticks
--- and to export everything.
---
--- TODO: We shouldn't rely on exports to find out what's in a ModGuts
--- https://github.com/ucsd-progsys/liquidhaskell/pull/2388#issuecomment-2411418479
+-- and to keep unused functions.
 desugarerDynFlags :: DynFlags -> DynFlags
 desugarerDynFlags df = (foldl gopt_unset df disabledOpts)
     { debugLevel   = 1                  -- To keep source note ticks
-    , backend      = interpreterBackend -- To export everything
+    , backend      = interpreterBackend -- To keep unused functions during desugaring
     }
   where
     disabledOpts =
-Original file line number
+Diff line change
@@ Expand Up / @@ -2,6 +2,8 @@ @@
     ## Next
+    - Simplify kvar solutions in fqout files [liquid-fixpoint#741](https://github.com/ucsd-progsys/liquid-fixpoint/pull/741).
     ## 0.9.10.1.2 (2025-03-06)
     - Implement opaque reflection, a feature to allow reflecting functions which
@@ Expand Down @@
+1 −1		.github/workflows/stan.yml
+111 −5		src/Language/Fixpoint/Solver.hs