Skip to content

Commit

Permalink
Enable hls-tactics-plugin tests in CI (#1474)
Browse files Browse the repository at this point in the history
* Enable hls-tactics-plugin tests in CI

* Revert a bug in `auto` that caused test failures
  • Loading branch information
isovector authored Mar 2, 2021
1 parent a70711a commit 00e3577
Show file tree
Hide file tree
Showing 4 changed files with 19 additions and 10 deletions.
5 changes: 5 additions & 0 deletions .github/workflows/test.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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"

Original file line number Diff line number Diff line change
Expand Up @@ -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 ()
Expand All @@ -29,7 +29,7 @@ known name t = do

deriveFmap :: TacticsM ()
deriveFmap = do
try' intros
try intros
overAlgebraicTerms homo
choice
[ overFunctions apply >> auto' 2
Expand Down
4 changes: 4 additions & 0 deletions plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Machinery.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 00e3577

Please sign in to comment.