Skip to content

Enable hls-tactics-plugin tests in CI #1474

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 6 commits into from
Mar 2, 2021
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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