From 31b5d0afdd7ee2178d11ef0797cea6aaf8ac4911 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Mon, 1 Mar 2021 11:34:52 -0800 Subject: [PATCH 1/2] Enable hls-tactics-plugin tests in CI --- .github/workflows/test.yml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 0589176ff0..9f71399e9d 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -119,3 +119,8 @@ jobs: # all functional test cases simultaneously which causes way too many hls # instances to be spun up for the poor github actions runner to handle run: cabal test wrapper-test --test-options="-j1" || cabal test wrapper-test --test-options="-j1" || cabal test wrapper-test --test-options="-j1" + + - name: Test hls-tactics-plugin test suite + if: ${{ matrix.test }} + run: LSP_TEST_LOG_COLOR=0 LSP_TEST_LOG_MESSAGES=true LSP_TEST_LOG_STDERR=true cabal test hls-tactics-plugin --test-options="-j1" + From 2ed0327668de60bfb130986a36bde200aaf1b940 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Tue, 2 Mar 2021 07:59:02 -0800 Subject: [PATCH 2/2] Revert a bug in `auto` that caused test failures --- .../src/Ide/Plugin/Tactic/KnownStrategies.hs | 18 +++++++++--------- .../src/Ide/Plugin/Tactic/Machinery.hs | 4 ++++ .../src/Ide/Plugin/Tactic/Tactics.hs | 2 +- 3 files changed, 14 insertions(+), 10 deletions(-) diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/KnownStrategies.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/KnownStrategies.hs index d0237acff2..d159dd03b5 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/KnownStrategies.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/KnownStrategies.hs @@ -2,14 +2,14 @@ module Ide.Plugin.Tactic.KnownStrategies where -import Control.Monad.Error.Class -import Ide.Plugin.Tactic.Context (getCurrentDefinitions) -import Ide.Plugin.Tactic.KnownStrategies.QuickCheck (deriveArbitrary) -import Ide.Plugin.Tactic.Machinery (tracing, try') -import Ide.Plugin.Tactic.Tactics -import Ide.Plugin.Tactic.Types -import OccName (mkVarOcc) -import Refinery.Tactic +import Control.Monad.Error.Class +import Ide.Plugin.Tactic.Context (getCurrentDefinitions) +import Ide.Plugin.Tactic.KnownStrategies.QuickCheck (deriveArbitrary) +import Ide.Plugin.Tactic.Machinery (tracing) +import Ide.Plugin.Tactic.Tactics +import Ide.Plugin.Tactic.Types +import OccName (mkVarOcc) +import Refinery.Tactic knownStrategies :: TacticsM () @@ -29,7 +29,7 @@ known name t = do deriveFmap :: TacticsM () deriveFmap = do - try' intros + try intros overAlgebraicTerms homo choice [ overFunctions apply >> auto' 2 diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs index 26c21dad62..30fc29cf42 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs @@ -278,6 +278,10 @@ requireConcreteHole m = do -- balloons the search space. This thing just tries it, but doesn't backtrack -- if it fails. -- +-- NOTE(sandy): But there's a bug! Or at least, something not understood here. +-- Using this everywhere breaks te tests, and neither I nor TOTBWF are sure +-- why. Prefer 'try' if you can, and only try this as a last resort. +-- -- TODO(sandy): Remove this when we upgrade to 0.4 try' :: Functor m diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs index 89cbea9b0d..3df6f235bf 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs @@ -319,7 +319,7 @@ auto' :: Int -> TacticsM () auto' 0 = throwError NoProgress auto' n = do let loop = auto' (n - 1) - try' intros + try intros choice [ overFunctions $ \fname -> do apply fname