diff --git a/Agda.cabal b/Agda.cabal --- a/Agda.cabal +++ b/Agda.cabal @@ -1,5 +1,5 @@ name: Agda -version: 2.5.4.1 +version: 2.5.4.2 cabal-version: >= 1.10 build-type: Custom license: OtherLicense @@ -36,7 +36,7 @@ tested-with: GHC == 7.10.3 GHC == 8.0.2 GHC == 8.2.2 - GHC == 8.4.3 + GHC == 8.4.4 extra-source-files: CHANGELOG.md README.md doc/user-manual.pdf @@ -44,7 +44,7 @@ stack-7.10.3.yaml stack-8.0.2.yaml stack-8.2.2.yaml - stack-8.4.3.yaml + stack-8.4.4.yaml data-dir: src/data data-files: Agda.css @@ -83,10 +83,10 @@ source-repository this type: git location: https://github.com/agda/agda.git - tag: v2.5.4.1 + tag: v2.5.4.2 flag cpphs - default: True + default: False manual: True description: Use cpphs instead of cpp. @@ -102,6 +102,8 @@ Enable the --count-clusters flag. (If enable-cluster-counting is False, then the --count-clusters flag triggers an error message.) +-- ASR (2018-09-14). Every new setup dependency should also be added +-- as a library dependency. See Issue #3225. custom-setup setup-depends: base >= 4.8.0.0 && < 4.12 , Cabal >= 1.22.5.0 && < 2.3 @@ -173,7 +175,6 @@ , stm >= 2.4.4 && < 2.5 , strict >= 0.3.2 && < 0.4 , template-haskell >= 2.10.0.0 && < 2.14 - , text >= 0.11.3.1 && < 1.3 , time >= 1.5.0.1 && < 1.9 , unordered-containers >= 0.2.5.0 && < 0.3 , uri-encode >= 1.5.0.4 && < 1.6 @@ -184,11 +185,21 @@ if impl(ghc >= 8.4) build-depends: transformers == 0.5.5.0 + -- ASR (2018-10-16). Required for supporting GHC 8.4.1, 8.4.2 and + -- 8.4.3. See Issue #3277. + if impl(ghc >= 8.4.1) && impl(ghc <= 8.4.3) + build-depends: text >= 1.2.3.0 && < 1.3 + else + build-depends: text >= 1.2.3.1 && < 1.3 + if impl(ghc >= 8.0) && impl(ghc < 8.4) build-depends: transformers == 0.5.2.0 + -- ASR (2018-09-14). We add the dependency on the filemanip library + -- due to Issue #3225. if impl(ghc >= 7.10) && impl(ghc < 8.0) - build-depends: transformers == 0.4.2.0 + build-depends: transformers == 0.4.2.0 + , filemanip >= 0.3.6.2 && < 0.4 -- zlib >= 0.6.1 is broken with GHC < 7.10.3. See Issue 1518. if impl(ghc < 7.10.3) @@ -359,6 +370,7 @@ Agda.TypeChecking.Free.Lazy Agda.TypeChecking.Free.Old Agda.TypeChecking.Free.Precompute + Agda.TypeChecking.Free.Reduce Agda.TypeChecking.Forcing Agda.TypeChecking.Functions Agda.TypeChecking.Implicit diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,26 @@ +Release notes for Agda version 2.5.4.2 +====================================== + +Installation and infrastructure +------------------------------- + +* Fixed installation with some old versions of `cabal-install` + [Issue [#3225](https://github.com/agda/agda/issues/3225)]. + +* Using `cpp` instead of `cpphs` as the default preprocessor + [Issue [#3223](https://github.com/agda/agda/issues/3223)]. + +* Added support for GHC 8.4.4. + +Other closed issues +-------------------- + +For 2.5.4.2 the following issues have also been closed +(see [bug tracker](https://github.com/agda/agda/issues)): + + - [#3199](https://github.com/agda/agda/issues/3199): Panics when serialising absolute paths + - [#3312](https://github.com/agda/agda/issues/3312): Crash in Substitute.hs + Release notes for Agda version 2.5.4.1 ====================================== @@ -872,7 +895,6 @@ - [#3090](https://github.com/agda/agda/issues/3090): Internal error in parser when using parentheses in BUILTIN pragma - [#3096](https://github.com/agda/agda/issues/3096): Support GHC 8.4.3 - Release notes for Agda version 2.5.3 ==================================== @@ -1695,7 +1717,6 @@ - [#2734](https://github.com/agda/agda/issues/2734): Make height of empty lines configurable - [#2736](https://github.com/agda/agda/issues/2736): Segfault using Alex 3.2.2 and cpphs - [#2740](https://github.com/agda/agda/issues/2740): Indenting every line of code should be a no-op - Release notes for Agda version 2.5.2 ==================================== diff --git a/doc/user-manual.pdf b/doc/user-manual.pdf Binary files a/doc/user-manual.pdf and b/doc/user-manual.pdf differ diff --git a/src/data/emacs-mode/agda2-mode-pkg.el b/src/data/emacs-mode/agda2-mode-pkg.el --- a/src/data/emacs-mode/agda2-mode-pkg.el +++ b/src/data/emacs-mode/agda2-mode-pkg.el @@ -1,2 +1,2 @@ -(define-package "agda2-mode" "2.5.4.1" +(define-package "agda2-mode" "2.5.4.2" "interactive development for Agda, a dependently typed functional programming language") diff --git a/src/data/emacs-mode/agda2-mode.el b/src/data/emacs-mode/agda2-mode.el --- a/src/data/emacs-mode/agda2-mode.el +++ b/src/data/emacs-mode/agda2-mode.el @@ -10,7 +10,7 @@ ;;; Code: -(defvar agda2-version "2.5.4.1" +(defvar agda2-version "2.5.4.2" "The version of the Agda mode. Note that the same version of the Agda executable must be used.") diff --git a/src/full/Agda/Compiler/Backend.hs b/src/full/Agda/Compiler/Backend.hs --- a/src/full/Agda/Compiler/Backend.hs +++ b/src/full/Agda/Compiler/Backend.hs @@ -37,7 +37,7 @@ import Agda.Interaction.Options import Agda.Interaction.FindFile import Agda.Interaction.Highlighting.HTML -import Agda.Interaction.Imports (getAllWarnings') +import Agda.Interaction.Imports (getAllWarnings) import Agda.TypeChecking.Warnings import Agda.Utils.FileName @@ -165,7 +165,7 @@ Just i -> sequence_ [ compilerMain backend isMain i | Backend backend <- backends ] -- print warnings that might have accumulated during compilation - ws <- filter (not . isUnsolvedWarning . tcWarning) <$> getAllWarnings' AllWarnings RespectFlags + ws <- filter (not . isUnsolvedWarning . tcWarning) <$> getAllWarnings AllWarnings unless (null ws) $ reportSDoc "warning" 1 $ P.vcat $ P.prettyTCM <$> ws diff --git a/src/full/Agda/Interaction/Imports.hs b/src/full/Agda/Interaction/Imports.hs --- a/src/full/Agda/Interaction/Imports.hs +++ b/src/full/Agda/Interaction/Imports.hs @@ -147,9 +147,9 @@ addImportedThings isig ibuiltin patsyns display userwarn warnings = do stImports %= \ imp -> unionSignatures [imp, isig] stImportedBuiltins %= \ imp -> Map.union imp ibuiltin + stImportedUserWarnings %= \ imp -> Map.union imp userwarn stPatternSynImports %= \ imp -> Map.union imp patsyns stImportedDisplayForms %= \ imp -> HMap.unionWith (++) imp display - stUserWarnings %= \ imp -> Map.union imp userwarn stTCWarnings %= \ imp -> List.union imp warnings addImportedInstances isig @@ -175,9 +175,9 @@ deriving (Functor, Foldable, Traversable) type MaybeWarnings = MaybeWarnings' [TCWarning] -applyFlagsToMaybeWarnings :: IgnoreFlags -> MaybeWarnings -> TCM MaybeWarnings -applyFlagsToMaybeWarnings r mw = do - w' <- traverse (applyFlagsToTCWarnings r) mw +applyFlagsToMaybeWarnings :: MaybeWarnings -> TCM MaybeWarnings +applyFlagsToMaybeWarnings mw = do + w' <- traverse applyFlagsToTCWarnings mw return $ if null w' then NoWarnings else w' instance Null a => Null (MaybeWarnings' a) where @@ -477,7 +477,7 @@ _ -> "Checking" withMsgs = bracket_ (chaseMsg checkMsg x $ Just $ filePath file) - (const $ do ws <- getAllWarnings' AllWarnings RespectFlags + (const $ do ws <- getAllWarnings AllWarnings let (we, wa) = classifyWarnings ws let wa' = filter ((Strict.Just file ==) . tcWarningOrigin) wa unless (null wa') $ @@ -503,7 +503,7 @@ isig <- use stImports ibuiltin <- use stImportedBuiltins display <- use stImportsDisplayForms - userwarn <- use stUserWarnings + userwarn <- use stImportedUserWarnings ipatsyns <- getPatternSynImports ho <- getInteractionOutputCallback -- Every interface is treated in isolation. Note: Some changes to @@ -752,7 +752,7 @@ stTokens .= mempty -- Grabbing warnings and unsolved metas to highlight them - warnings <- getAllWarnings' AllWarnings RespectFlags + warnings <- getAllWarnings AllWarnings unless (null warnings) $ reportSDoc "import.iface.create" 20 $ P.text "collected warnings: " P.<> prettyTCM warnings unsolved <- getAllUnsolved @@ -812,10 +812,7 @@ ] reportSLn "import.iface.create" 7 $ "Finished serialization." - mallWarnings <- getAllWarnings ErrorWarnings - $ case isMain of - MainInterface _ -> IgnoreFlags - NotMainInterface -> RespectFlags + mallWarnings <- getMaybeWarnings' isMain ErrorWarnings reportSLn "import.iface.create" 7 $ "Considering writing to interface file." case (mallWarnings, isMain) of @@ -844,11 +841,6 @@ return $ first constructIScope (i, mallWarnings) --- | Collect all warnings that have accumulated in the state. --- Depending on the argument, we either respect the flags passed --- in by the user, or not (for instance when deciding if we are --- writing an interface file or not) - getUniqueMetasRanges :: [MetaId] -> TCM [Range] getUniqueMetasRanges = fmap List.nub . mapM getMetaRange @@ -871,8 +863,18 @@ , checkNonEmpty UnsolvedMetaVariables unsolvedMetas , checkNonEmpty UnsolvedConstraints unsolvedConstraints ] -getAllWarnings' :: WhichWarnings -> IgnoreFlags -> TCM [TCWarning] -getAllWarnings' ww ifs = do + +-- | Collect all warnings that have accumulated in the state. + +getAllWarnings :: WhichWarnings -> TCM [TCWarning] +getAllWarnings = getAllWarnings' NotMainInterface + +-- | Expert version of 'getAllWarnings'; if 'isMain' is a +-- 'MainInterface', the warnings definitely include also unsolved +-- warnings. + +getAllWarnings' :: MainInterface -> WhichWarnings -> TCM [TCWarning] +getAllWarnings' isMain ww = do unsolved <- getAllUnsolved collectedTCWarnings <- use stTCWarnings @@ -880,12 +882,15 @@ not (null unsolved && onlyShowIfUnsolved w) fmap (filter (showWarn . tcWarning)) - $ applyFlagsToTCWarnings ifs $ reverse + $ applyFlagsToTCWarnings' isMain $ reverse $ unsolved ++ collectedTCWarnings -getAllWarnings :: WhichWarnings -> IgnoreFlags -> TCM MaybeWarnings -getAllWarnings ww ifs = do - allWarnings <- getAllWarnings' ww ifs +getMaybeWarnings :: WhichWarnings -> TCM MaybeWarnings +getMaybeWarnings = getMaybeWarnings' NotMainInterface + +getMaybeWarnings' :: MainInterface -> WhichWarnings -> TCM MaybeWarnings +getMaybeWarnings' isMain ww = do + allWarnings <- getAllWarnings' isMain ww return $ if null allWarnings -- Andreas, issue 964: not checking null interactionPoints -- anymore; we want to serialize with open interaction points now! @@ -898,7 +903,7 @@ NonFatalErrors{} -> return [] _ -> localState $ do put tcst - ws <- getAllWarnings' ErrorWarnings RespectFlags + ws <- getAllWarnings AllWarnings -- We filter out the unsolved(Metas/Constraints) to stay -- true to the previous error messages. return $ filter (not . isUnsolvedWarning . tcWarning) ws @@ -946,7 +951,7 @@ display <- HMap.filter (not . null) . HMap.map (filter isClosed) <$> use stImportsDisplayForms -- TODO: Kill some ranges? (display, sig) <- eliminateDeadCode display =<< getSignature - userwarns <- use stUserWarnings + userwarns <- use stLocalUserWarnings syntaxInfo <- use stSyntaxInfo -- Andreas, 2015-02-09 kill ranges in pattern synonyms before -- serialization to avoid error locations pointing to external files @@ -954,7 +959,7 @@ patsyns <- killRange <$> getPatternSyns h <- liftIO $ hashFile file let builtin' = Map.mapWithKey (\ x b -> (x,) . primFunName <$> b) builtin - warnings <- getAllWarnings' AllWarnings RespectFlags + warnings <- getAllWarnings AllWarnings reportSLn "import.iface" 7 " instantiating all meta variables" i <- instantiateFull $ Interface { iSourceHash = h diff --git a/src/full/Agda/Interaction/Imports.hs-boot b/src/full/Agda/Interaction/Imports.hs-boot --- a/src/full/Agda/Interaction/Imports.hs-boot +++ b/src/full/Agda/Interaction/Imports.hs-boot @@ -6,4 +6,10 @@ import Agda.TypeChecking.Monad.Base ( TCM ) import Data.Map ( Map ) +data Mode + +data MainInterface = MainInterface Mode | NotMainInterface + +instance Eq MainInterface + scopeCheckImport :: ModuleName -> TCM (ModuleName, Map ModuleName Scope) diff --git a/src/full/Agda/Interaction/InteractionTop.hs b/src/full/Agda/Interaction/InteractionTop.hs --- a/src/full/Agda/Interaction/InteractionTop.hs +++ b/src/full/Agda/Interaction/InteractionTop.hs @@ -755,7 +755,7 @@ (if b == QuickLaTeX then Imp.ScopeCheck else Imp.TypeCheck) $ \(i, mw) -> do - mw <- lift $ Imp.applyFlagsToMaybeWarnings RespectFlags mw + mw <- lift $ Imp.applyFlagsToMaybeWarnings mw case mw of Imp.NoWarnings -> do lift $ case b of @@ -1054,7 +1054,7 @@ -- | Show warnings interpretWarnings :: CommandM (String, String) interpretWarnings = do - mws <- lift $ Imp.getAllWarnings AllWarnings RespectFlags + mws <- lift $ Imp.getMaybeWarnings AllWarnings case filter isNotMeta <$> mws of Imp.SomeWarnings ws@(_:_) -> do let (we, wa) = classifyWarnings ws diff --git a/src/full/Agda/Interaction/Options.hs b/src/full/Agda/Interaction/Options.hs --- a/src/full/Agda/Interaction/Options.hs +++ b/src/full/Agda/Interaction/Options.hs @@ -2,7 +2,6 @@ module Agda.Interaction.Options ( CommandLineOptions(..) - , IgnoreFlags(..) , PragmaOptions(..) , OptionsPragma , Flag, OptM, runOptM, OptDescr(..), ArgDescr(..) @@ -60,8 +59,10 @@ ) import Agda.Utils.FileName ( absolute, AbsolutePath, filePath ) -import Agda.Utils.Monad ( ifM, readM ) +import Agda.Utils.Functor ( (<&>) ) +import Agda.Utils.Lens ( Lens', over ) import Agda.Utils.List ( groupOn, wordsBy ) +import Agda.Utils.Monad ( ifM, readM ) import Agda.Utils.String ( indent ) import Agda.Utils.Trie ( Trie ) import Agda.Syntax.Parser.Literate ( literateExts ) @@ -81,11 +82,6 @@ type Verbosity = Trie String Int --- ignore or respect the flags --allow-unsolved-metas, --- --no-termination-check, --no-positivity-check? -data IgnoreFlags = IgnoreFlags | RespectFlags - deriving Eq - -- Don't forget to update -- doc/user-manual/tools/command-line-options.rst -- if you make changes to the command-line options! @@ -375,7 +371,11 @@ ignoreInterfacesFlag o = return $ o { optIgnoreInterfaces = True } allowUnsolvedFlag :: Flag PragmaOptions -allowUnsolvedFlag o = return $ o { optAllowUnsolved = True } +allowUnsolvedFlag o = do + let upd = over warningSet (Set.\\ unsolvedWarnings) + return $ o { optAllowUnsolved = True + , optWarningMode = upd (optWarningMode o) + } showImplicitFlag :: Flag PragmaOptions showImplicitFlag o = return $ o { optShowImplicit = True } @@ -419,10 +419,18 @@ latexDirFlag d o = return $ o { optLaTeXDir = d } noPositivityFlag :: Flag PragmaOptions -noPositivityFlag o = return $ o { optDisablePositivity = True } +noPositivityFlag o = do + let upd = over warningSet (Set.delete NotStrictlyPositive_) + return $ o { optDisablePositivity = True + , optWarningMode = upd (optWarningMode o) + } dontTerminationCheckFlag :: Flag PragmaOptions -dontTerminationCheckFlag o = return $ o { optTerminationCheck = False } +dontTerminationCheckFlag o = do + let upd = over warningSet (Set.delete TerminationIssue_) + return $ o { optTerminationCheck = False + , optWarningMode = upd (optWarningMode o) + } -- The option was removed. See Issue 1918. dontCompletenessCheckFlag :: Flag PragmaOptions @@ -430,8 +438,8 @@ throwError "the --no-coverage-check option has been removed" dontUniverseCheckFlag :: Flag PragmaOptions -dontUniverseCheckFlag o = return $ o { optUniverseCheck = False - } +dontUniverseCheckFlag o = return $ o { optUniverseCheck = False } + etaFlag :: Flag PragmaOptions etaFlag o = return $ o { optEta = True } @@ -475,10 +483,18 @@ noPatternMatchingFlag o = return $ o { optPatternMatching = False } exactSplitFlag :: Flag PragmaOptions -exactSplitFlag o = return $ o { optExactSplit = True } +exactSplitFlag o = do + let upd = over warningSet (Set.insert CoverageNoExactSplit_) + return $ o { optExactSplit = True + , optWarningMode = upd (optWarningMode o) + } noExactSplitFlag :: Flag PragmaOptions -noExactSplitFlag o = return $ o { optExactSplit = False } +noExactSplitFlag o = do + let upd = over warningSet (Set.delete CoverageNoExactSplit_) + return $ o { optExactSplit = False + , optWarningMode = upd (optWarningMode o) + } rewritingFlag :: Flag PragmaOptions rewritingFlag o = return $ o { optRewriting = True } @@ -497,10 +513,11 @@ return $ o { optInversionMaxDepth = d } interactiveFlag :: Flag CommandLineOptions -interactiveFlag o = return $ o { optInteractive = True - , optPragmaOptions = (optPragmaOptions o) - { optAllowUnsolved = True } - } +interactiveFlag o = do + prag <- allowUnsolvedFlag (optPragmaOptions o) + return $ o { optInteractive = True + , optPragmaOptions = prag + } compileFlagNoMain :: Flag PragmaOptions compileFlagNoMain o = return $ o { optCompileNoMain = True } diff --git a/src/full/Agda/Interaction/Options/Warnings.hs b/src/full/Agda/Interaction/Options/Warnings.hs --- a/src/full/Agda/Interaction/Options/Warnings.hs +++ b/src/full/Agda/Interaction/Options/Warnings.hs @@ -6,6 +6,11 @@ , warningSet , warn2Error , defaultWarningSet + , allWarnings + , usualWarnings + , noWarnings + , unsolvedWarnings + , errorWarnings , defaultWarningMode , warningModeUpdate , warningSets @@ -75,18 +80,46 @@ warningSets :: [(String, (Set WarningName, String))] warningSets = [ ("all" , (allWarnings, "All of the existing warnings")) , ("warn" , (usualWarnings, "Default warning level")) - , ("ignore", (noWarnings, "Ignore all warnings")) + , ("ignore", (errorWarnings, "Ignore all the benign warnings")) ] noWarnings :: Set WarningName noWarnings = Set.empty +unsolvedWarnings :: Set WarningName +unsolvedWarnings = Set.fromList + [ UnsolvedMetaVariables_ + , UnsolvedInteractionMetas_ + , UnsolvedConstraints_ + ] + +errorWarnings :: Set WarningName +errorWarnings = Set.fromList + [ CoverageIssue_ + , GenericNonFatalError_ + , NotStrictlyPositive_ + , OverlappingTokensWarning_ + , SafeFlagPostulate_ + , SafeFlagPragma_ + , SafeFlagNonTerminating_ + , SafeFlagTerminating_ + , SafeFlagPrimTrustMe_ + , SafeFlagNoPositivityCheck_ + , SafeFlagPolarity_ + , TerminationIssue_ + , UnsolvedMetaVariables_ + , UnsolvedInteractionMetas_ + , UnsolvedConstraints_ + ] + allWarnings :: Set WarningName allWarnings = Set.fromList [minBound..maxBound] usualWarnings :: Set WarningName usualWarnings = allWarnings Set.\\ Set.fromList - [ UnknownFixityInMixfixDecl_ ] + [ UnknownFixityInMixfixDecl_ + , CoverageNoExactSplit_ + ] -- | The @WarningName@ data enumeration is meant to have a one-to-one correspondance -- to existing warnings in the codebase. diff --git a/src/full/Agda/Main.hs b/src/full/Agda/Main.hs --- a/src/full/Agda/Main.hs +++ b/src/full/Agda/Main.hs @@ -143,7 +143,7 @@ (Imp.ScopeCheck, _) -> return Nothing (_, NoWarnings) -> return $ Just i (_, SomeWarnings ws) -> do - ws' <- applyFlagsToTCWarnings RespectFlags ws + ws' <- applyFlagsToTCWarnings ws case ws' of [] -> return Nothing cuws -> tcWarningsToError cuws @@ -160,7 +160,7 @@ LaTeX.generateLaTeX i -- Print accumulated warnings - ws <- (snd . classifyWarnings) <$> Imp.getAllWarnings' AllWarnings RespectFlags + ws <- (snd . classifyWarnings) <$> Imp.getAllWarnings AllWarnings unless (null ws) $ do let banner = text $ "\n" ++ delimiter "All done; warnings encountered" reportSDoc "warning" 1 $ diff --git a/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs b/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs --- a/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs +++ b/src/full/Agda/Syntax/Translation/ConcreteToAbstract.hs @@ -514,7 +514,7 @@ -- In case we find a defined name, we start by checking whether there's -- a warning attached to it reportSDoc "scope.warning" 50 $ text $ "Checking usage of " ++ prettyShow d - mstr <- Map.lookup (anameName d) <$> use stUserWarnings + mstr <- Map.lookup (anameName d) <$> getUserWarnings forM_ mstr (warning . UserWarning) -- and then we return the name return $ nameExpr d @@ -1911,7 +1911,7 @@ toAbstract (C.WarningOnUsage _ oqn str) = do qn <- toAbstract $ OldName oqn - stUserWarnings %= Map.insert qn str + stLocalUserWarnings %= Map.insert qn str pure [] -- Termination checking pragmes are handled by the nicifier diff --git a/src/full/Agda/TypeChecking/Errors.hs b/src/full/Agda/TypeChecking/Errors.hs --- a/src/full/Agda/TypeChecking/Errors.hs +++ b/src/full/Agda/TypeChecking/Errors.hs @@ -10,6 +10,7 @@ , prettyTCWarnings' , prettyTCWarnings , tcWarningsToError + , applyFlagsToTCWarnings' , applyFlagsToTCWarnings , dropTopLevelModule , stringTCErr @@ -33,7 +34,9 @@ import qualified Data.Map as Map import qualified Text.PrettyPrint.Boxes as Boxes +import {-# SOURCE #-} Agda.Interaction.Imports (MainInterface(..)) import Agda.Interaction.Options +import Agda.Interaction.Options.Warnings import Agda.Syntax.Common import Agda.Syntax.Fixity import Agda.Syntax.Notation @@ -60,11 +63,13 @@ import Agda.TypeChecking.Substitute import Agda.TypeChecking.Telescope ( ifPiType ) import Agda.TypeChecking.Reduce (instantiate) +import Agda.TypeChecking.Warnings import Agda.Utils.Except ( MonadError(catchError, throwError) ) import Agda.Utils.FileName import Agda.Utils.Function import Agda.Utils.Functor +import Agda.Utils.Lens import Agda.Utils.List import Agda.Utils.Maybe import Agda.Utils.Monad @@ -236,8 +241,8 @@ -- | Depending which flags are set, one may happily ignore some -- warnings. -applyFlagsToTCWarnings :: IgnoreFlags -> [TCWarning] -> TCM [TCWarning] -applyFlagsToTCWarnings ifs ws = do +applyFlagsToTCWarnings' :: MainInterface -> [TCWarning] -> TCM [TCWarning] +applyFlagsToTCWarnings' isMain ws = do -- For some reason some SafeFlagPragma seem to be created multiple times. -- This is a way to collect all of them and remove duplicates. @@ -247,45 +252,28 @@ [TCWarning r (SafeFlagPragma sfp) p b] _ -> [] - - unsolvedNotOK <- not . optAllowUnsolved <$> pragmaOptions - negativeNotOK <- not . optDisablePositivity <$> pragmaOptions - loopingNotOK <- optTerminationCheck <$> pragmaOptions - catchallNotOK <- optExactSplit <$> pragmaOptions + warnSet <- do + opts <- pragmaOptions + let warnSet = optWarningMode opts ^. warningSet + pure $ if isMain /= NotMainInterface + then Set.union warnSet unsolvedWarnings + else warnSet -- filter out the warnings the flags told us to ignore - let cleanUp w = - let ignore = ifs == IgnoreFlags - keepUnsolved us = not (null us) && (ignore || unsolvedNotOK) - in case w of - TerminationIssue{} -> ignore || loopingNotOK - CoverageIssue{} -> ignore || unsolvedNotOK - NotStrictlyPositive{} -> ignore || negativeNotOK - UnsolvedMetaVariables ums -> keepUnsolved ums - UnsolvedInteractionMetas uis -> keepUnsolved uis - UnsolvedConstraints ucs -> keepUnsolved ucs - OldBuiltin{} -> True - EmptyRewritePragma -> True - UselessPublic -> True - ParseWarning{} -> True - UnreachableClauses{} -> True - InversionDepthReached{} -> True - CoverageNoExactSplit{} -> catchallNotOK - UselessInline{} -> True - GenericWarning{} -> True - GenericNonFatalError{} -> True - SafeFlagPostulate{} -> True - SafeFlagPragma{} -> False -- dealt with separately - SafeFlagNonTerminating -> True - SafeFlagTerminating -> True - SafeFlagPrimTrustMe -> True - SafeFlagNoPositivityCheck -> True - SafeFlagPolarity -> True - DeprecationWarning{} -> True - NicifierIssue{} -> True - UserWarning{} -> True + let cleanUp w = let wName = warningName w in + wName /= SafeFlagPragma_ + && wName `elem` warnSet + && case w of + UnsolvedMetaVariables ums -> not $ null ums + UnsolvedInteractionMetas uis -> not $ null uis + UnsolvedConstraints ucs -> not $ null ucs + _ -> True + return $ sfp ++ filter (cleanUp . tcWarning) ws + +applyFlagsToTCWarnings :: [TCWarning] -> TCM [TCWarning] +applyFlagsToTCWarnings = applyFlagsToTCWarnings' NotMainInterface --------------------------------------------------------------------------- -- * Helpers diff --git a/src/full/Agda/TypeChecking/Free/Reduce.hs b/src/full/Agda/TypeChecking/Free/Reduce.hs new file mode 100644 --- /dev/null +++ b/src/full/Agda/TypeChecking/Free/Reduce.hs @@ -0,0 +1,117 @@ +-- | Free variable check that reduces the subject to make certain variables not +-- free. Used when pruning metavariables in Agda.TypeChecking.MetaVars.Occurs. +module Agda.TypeChecking.Free.Reduce (forceNotFree) where + +import Control.Monad.State +import qualified Data.IntSet as IntSet +import Data.IntSet (IntSet) +import Data.Traversable (traverse) + +import Agda.Syntax.Common +import Agda.Syntax.Internal +import Agda.TypeChecking.Monad +import Agda.TypeChecking.Reduce +import Agda.TypeChecking.Substitute +import Agda.TypeChecking.Free.Precompute +import Agda.Utils.Monad + +-- | Try to enforce a set of variables not occurring in a given type. Returns a +-- possibly reduced version of the type and the subset of variables that does +-- indeed not occur in the reduced type. +forceNotFree :: IntSet -> Type -> TCM (IntSet, Type) +forceNotFree xs a = do + (a, xs) <- runStateT (forceNotFreeR $ precomputeFreeVars_ a) xs + return (xs, a) + +class (PrecomputeFreeVars a, Subst Term a) => ForceNotFree a where + -- Reduce the argument if necessary, to make as many as possible of the + -- variables in the state not free. Updates the state, removing the variables + -- that couldn't be make not free. By updating the state as soon as a + -- variable can not be reduced away, we avoid trying to get rid of it in + -- other places. + forceNotFree' :: a -> StateT IntSet TCM a + +-- Reduce the argument if there are offending free variables. Doesn't call the +-- continuation when no reduction is required. +reduceIfFreeVars :: (Reduce a, ForceNotFree a) => (a -> StateT IntSet TCM a) -> a -> StateT IntSet TCM a +reduceIfFreeVars k a = do + xs <- get + let fvs = precomputedFreeVars a + notfree = IntSet.null $ IntSet.intersection xs fvs + if | notfree -> return a + | otherwise -> k . precomputeFreeVars_ =<< lift (reduce a) + +-- Careful not to define forceNotFree' = forceNotFreeR since that would loop. +forceNotFreeR :: (Reduce a, ForceNotFree a) => a -> StateT IntSet TCM a +forceNotFreeR = reduceIfFreeVars forceNotFree' + +instance (Reduce a, ForceNotFree a) => ForceNotFree (Arg a) where + -- Precomputed free variables are stored in the Arg so reduceIf outside the + -- traverse. + forceNotFree' = reduceIfFreeVars (traverse forceNotFree') + +instance (Reduce a, ForceNotFree a) => ForceNotFree (Dom a) where + forceNotFree' = traverse forceNotFreeR + +instance (Reduce a, ForceNotFree a) => ForceNotFree (Abs a) where + -- Reduction stops at abstractions (lambda/pi) so do reduceIf/forceNotFreeR here. + forceNotFree' a@NoAbs{} = traverse forceNotFreeR a + forceNotFree' a@Abs{} = + -- Shift variables up when going under the abstraction and back down when + -- coming out of it. Since we only ever remove variables from the state + -- there's no danger of getting negative indices. + reduceIfFreeVars (bracket_ (modify $ IntSet.map succ) (\ _ -> modify $ IntSet.map pred) . + traverse forceNotFree') a + +instance ForceNotFree a => ForceNotFree [a] where + forceNotFree' = traverse forceNotFree' + +instance (Reduce a, ForceNotFree a) => ForceNotFree (Elim' a) where + -- There's an Arg inside Elim' which stores precomputed free vars, so let's + -- not skip over that. + forceNotFree' (Apply arg) = Apply <$> forceNotFree' arg + forceNotFree' e@Proj{} = return e + +instance ForceNotFree Type where + forceNotFree' (El s t) = El <$> forceNotFree' s <*> forceNotFree' t + +instance ForceNotFree Term where + forceNotFree' t = case t of + Var x es -> Var x <$ modify (IntSet.delete x) <*> forceNotFree' es + Def f es -> Def f <$> forceNotFree' es + Con c h es -> Con c h <$> forceNotFree' es + MetaV x es -> MetaV x <$> forceNotFree' es + Lam h b -> Lam h <$> forceNotFree' b + Pi a b -> Pi <$> forceNotFree' a <*> forceNotFree' b -- Dom and Abs do reduceIf so not needed here + Sort s -> Sort <$> forceNotFree' s + Level l -> Level <$> forceNotFree' l + DontCare t -> DontCare <$> forceNotFreeR t -- Reduction stops at DontCare so reduceIf + Lit{} -> return t + +instance ForceNotFree Level where + forceNotFree' (Max as) = Max <$> forceNotFree' as + +instance ForceNotFree PlusLevel where + forceNotFree' l = case l of + ClosedLevel{} -> return l + Plus k a -> Plus k <$> forceNotFree' a + +instance ForceNotFree LevelAtom where + forceNotFree' l = case l of + MetaLevel x es -> MetaLevel x <$> forceNotFree' es + BlockedLevel x t -> BlockedLevel x <$> forceNotFree' t + NeutralLevel b t -> NeutralLevel b <$> forceNotFree' t + UnreducedLevel t -> UnreducedLevel <$> forceNotFreeR t -- Already reduce in the cases above + +instance ForceNotFree Sort where + -- Reduce for sorts already goes under all sort constructors, so we can get + -- away without forceNotFreeR here. + forceNotFree' s = case s of + Type l -> Type <$> forceNotFree' l + Prop -> return Prop + PiSort a b -> PiSort <$> forceNotFree' a <*> forceNotFree' b + UnivSort s -> UnivSort <$> forceNotFree' s + MetaS x es -> MetaS x <$> forceNotFree' es + Inf -> return s + SizeUniv -> return s + diff --git a/src/full/Agda/TypeChecking/MetaVars/Occurs.hs b/src/full/Agda/TypeChecking/MetaVars/Occurs.hs --- a/src/full/Agda/TypeChecking/MetaVars/Occurs.hs +++ b/src/full/Agda/TypeChecking/MetaVars/Occurs.hs @@ -23,6 +23,8 @@ import Data.Monoid import Data.Set (Set) import qualified Data.Set as Set +import qualified Data.IntSet as IntSet +import Data.IntSet (IntSet) import Data.Traversable (traverse) import qualified Agda.Benchmarking as Bench @@ -35,11 +37,11 @@ import Agda.TypeChecking.Reduce import Agda.TypeChecking.Pretty import Agda.TypeChecking.Free hiding (Occurrence(..)) +import Agda.TypeChecking.Free.Reduce import Agda.TypeChecking.Substitute import Agda.TypeChecking.Datatypes import Agda.TypeChecking.Records import {-# SOURCE #-} Agda.TypeChecking.MetaVars --- import Agda.TypeChecking.MetaVars import Agda.Utils.Either @@ -716,7 +718,7 @@ let a = jMetaType $ mvJudgement mv TelV tel b <- telView' <$> instantiateFull a let args = zip (telToList tel) (kills ++ repeat False) - (kills', a') = killedType args b + (kills', a') <- killedType args b dbg kills' a a' -- If there is any prunable argument, perform the pruning if not (any unArg kills') then return PrunedNothing else do @@ -748,14 +750,79 @@ -- Invariant: @k'i == True@ iff @ki == True@ and pruning the @i@th argument from -- type @b@ is possible without creating unbound variables. -- @t'@ is type @t@ after pruning all @k'i==True@. -killedType :: [(Dom (ArgName, Type), Bool)] -> Type -> ([Arg Bool], Type) -killedType [] b = ([], b) -killedType ((arg@(Dom info _), kill) : kills) b - | dontKill = (Arg info False : args, mkPi arg b') - | otherwise = (Arg info True : args, strengthen __IMPOSSIBLE__ b') +killedType :: [(Dom (ArgName, Type), Bool)] -> Type -> TCM ([Arg Bool], Type) +killedType args b = do + + -- Turn list of bools into an IntSet containing the variables we want to kill + -- (indices relative to b). + let tokill = IntSet.fromList [ i | ((_, True), i) <- zip (reverse args) [0..] ] + + -- First, check the free variables of b to see if they prevent any kills. + (tokill, b) <- reallyNotFreeIn tokill b + + -- Then recurse over the telescope (right-to-left), building up the final type. + (killed, b) <- go (reverse $ map fst args) tokill b + + -- Turn the IntSet of killed variables into the list of Arg Bool's to return. + let kills = [ Arg (getArgInfo dom) (IntSet.member i killed) + | (i, (dom, _)) <- reverse $ zip [0..] $ reverse args ] + return (kills, b) where - (args, b') = killedType kills b - dontKill = not kill || 0 `freeIn` b' + down = IntSet.map pred + up = IntSet.map succ + + -- go Δ xs B + -- Invariants: + -- - Δ ⊢ B + -- - Δ is represented as a list in right-to-left order + -- - xs are deBruijn indices into Δ + -- - xs ∩ FV(B) = Ø + -- Result: (ys, Δ' → B') + -- where Δ' ⊆ Δ (possibly reduced to remove dependencies, see #3177) + -- ys ⊆ xs are the variables that were dropped from Δ + -- B' = strengthen ys B + go :: [Dom (ArgName, Type)] -> IntSet -> Type -> TCM (IntSet, Type) + go [] xs b | IntSet.null xs = return (xs, b) + | otherwise = __IMPOSSIBLE__ + go (arg : args) xs b -- go (Δ (x : A)) xs B, (x = deBruijn index 0) + | IntSet.member 0 xs = do + -- Case x ∈ xs. We know x ∉ FV(B), so we can safely drop x from the + -- telescope. Drop x from xs (and shift indices) and recurse with + -- `strengthen x B`. + let ys = down (IntSet.delete 0 xs) + (ys, b) <- go args ys $ strengthen __IMPOSSIBLE__ b + -- We need to return a set of killed variables relative to Δ (x : A), so + -- shift ys and add x back in. + return (IntSet.insert 0 $ up ys, b) + | otherwise = do + -- Case x ∉ xs. We either can't or don't want to get rid of x. In + -- this case we have to check A for potential dependencies preventing + -- us from killing variables in xs. + let xs' = down xs -- Shift to make relative to Δ ⊢ A + (name, a) = unDom arg + (ys, a) <- reallyNotFreeIn xs' a + -- Recurse on Δ, ys, and (x : A') → B, where A reduces to A' and ys ⊆ xs' + -- not free in A'. We already know ys not free in B. + (zs, b) <- go args ys (mkPi ((name, a) <$ arg) b) + -- Shift back up to make it relative to Δ (x : A) again. + return (up zs, b) + +reallyNotFreeIn :: IntSet -> Type -> TCM (IntSet, Type) +reallyNotFreeIn xs a | IntSet.null xs = return (xs, a) -- Shortcut +reallyNotFreeIn xs a = do + let fvs = freeVars a + anywhere = allVars fvs + rigid = IntSet.unions [stronglyRigidVars fvs, unguardedVars fvs] + nonrigid = IntSet.difference anywhere rigid + hasNo = IntSet.null . IntSet.intersection xs + if | hasNo nonrigid -> + -- No non-rigid occurrences. We can't do anything about the rigid + -- occurrences so drop those and leave `a` untouched. + return (IntSet.difference xs rigid, a) + | otherwise -> do + -- If there are non-rigid occurrences we need to reduce a to see if + -- we can get rid of them (#3177). + forceNotFree (IntSet.difference xs rigid) a -- | Instantiate a meta variable with a new one that only takes -- the arguments which are not pruneable. diff --git a/src/full/Agda/TypeChecking/Monad/Base.hs b/src/full/Agda/TypeChecking/Monad/Base.hs --- a/src/full/Agda/TypeChecking/Monad/Base.hs +++ b/src/full/Agda/TypeChecking/Monad/Base.hs @@ -143,7 +143,10 @@ -- ^ @{-# FOREIGN #-}@ code that should be included in the compiled output. -- Does not include code for imported modules. , stPreFreshInteractionId :: !InteractionId - , stPreUserWarnings :: !(Map A.QName String) + , stPreImportedUserWarnings :: !(Map A.QName String) + -- ^ Imported @UserWarning@s, not to be stored in the @Interface@ + , stPreLocalUserWarnings :: !(Map A.QName String) + -- ^ Locally defined @UserWarning@s, to be stored in the @Interface@ } type DisambiguatedNames = IntMap A.QName @@ -287,7 +290,8 @@ , stPreImportedInstanceDefs = Map.empty , stPreForeignCode = Map.empty , stPreFreshInteractionId = 0 - , stPreUserWarnings = Map.empty + , stPreImportedUserWarnings = Map.empty + , stPreLocalUserWarnings = Map.empty } initPostScopeState :: PostScopeState @@ -388,10 +392,21 @@ f (stPreFreshInteractionId (stPreScopeState s)) <&> \x -> s {stPreScopeState = (stPreScopeState s) {stPreFreshInteractionId = x}} -stUserWarnings :: Lens' (Map A.QName String) TCState -stUserWarnings f s = - f (stPreUserWarnings (stPreScopeState s)) <&> - \ x -> s {stPreScopeState = (stPreScopeState s) {stPreUserWarnings = x}} +stImportedUserWarnings :: Lens' (Map A.QName String) TCState +stImportedUserWarnings f s = + f (stPreImportedUserWarnings (stPreScopeState s)) <&> + \ x -> s {stPreScopeState = (stPreScopeState s) {stPreImportedUserWarnings = x}} + +stLocalUserWarnings :: Lens' (Map A.QName String) TCState +stLocalUserWarnings f s = + f (stPreLocalUserWarnings (stPreScopeState s)) <&> + \ x -> s {stPreScopeState = (stPreScopeState s) {stPreLocalUserWarnings = x}} + +getUserWarnings :: MonadState TCState m => m (Map A.QName String) +getUserWarnings = do + iuw <- use stImportedUserWarnings + luw <- use stLocalUserWarnings + return $ iuw `Map.union` luw stBackends :: Lens' [Backend] TCState stBackends f s = diff --git a/src/full/Agda/TypeChecking/Serialise.hs b/src/full/Agda/TypeChecking/Serialise.hs --- a/src/full/Agda/TypeChecking/Serialise.hs +++ b/src/full/Agda/TypeChecking/Serialise.hs @@ -60,7 +60,7 @@ -- 32-bit machines). Word64 does not have these problems. currentInterfaceVersion :: Word64 -currentInterfaceVersion = 20180518 * 10 + 0 +currentInterfaceVersion = 20181021 * 10 + 0 -- | Encodes something. To ensure relocatability file paths in -- positions are replaced with module names. diff --git a/src/full/Agda/TypeChecking/Serialise/Instances/Errors.hs b/src/full/Agda/TypeChecking/Serialise/Instances/Errors.hs --- a/src/full/Agda/TypeChecking/Serialise/Instances/Errors.hs +++ b/src/full/Agda/TypeChecking/Serialise/Instances/Errors.hs @@ -35,7 +35,6 @@ icod_ (TerminationIssue a) = __IMPOSSIBLE__ icod_ (UnreachableClauses a b) = icodeN 0 UnreachableClauses a b icod_ (CoverageIssue a b) = __IMPOSSIBLE__ - icod_ (CoverageNoExactSplit a b) = __IMPOSSIBLE__ icod_ (NotStrictlyPositive a b) = __IMPOSSIBLE__ icod_ (UnsolvedMetaVariables a) = __IMPOSSIBLE__ icod_ (UnsolvedInteractionMetas a) = __IMPOSSIBLE__ @@ -58,6 +57,7 @@ icod_ (NicifierIssue a) = icodeN 7 NicifierIssue a icod_ (InversionDepthReached a) = icodeN 8 InversionDepthReached a icod_ (UserWarning a) = icodeN 9 UserWarning a + icod_ (CoverageNoExactSplit a b) = icodeN 10 CoverageNoExactSplit a b value = vcase valu where valu [0, a, b] = valuN UnreachableClauses a b @@ -70,6 +70,7 @@ valu [7, a] = valuN NicifierIssue a valu [8, a] = valuN InversionDepthReached a valu [9, a] = valuN UserWarning a + valu [10, a, b] = valuN CoverageNoExactSplit a b valu _ = malformed instance EmbPrj DeclarationWarning where diff --git a/src/full/Agda/TypeChecking/Warnings.hs b/src/full/Agda/TypeChecking/Warnings.hs --- a/src/full/Agda/TypeChecking/Warnings.hs +++ b/src/full/Agda/TypeChecking/Warnings.hs @@ -5,7 +5,7 @@ import qualified Data.Set as Set import qualified Data.List as List import Data.Maybe ( catMaybes ) -import Control.Monad (guard, forM_) +import Control.Monad ( guard, forM, unless ) import Agda.TypeChecking.Monad.Base import Agda.TypeChecking.Monad.Caching @@ -62,12 +62,18 @@ | onlyOnce w && elem tcwarn tcwarns = tcwarns -- Eq on TCWarning only checks head constructor | otherwise = tcwarn : tcwarns - forM_ (catMaybes $ applyWarningMode wmode <$> ws) $ \ w' -> do + -- We collect *all* of the warnings no matter whether they are in the @warningSet@ + -- or not. If we find one which should be turned into an error, we keep processing + -- the rest of the warnings and *then* report all of the errors at once. + merrs <- forM ws $ \ w' -> do tcwarn <- warning_ w' - if wmode ^. warn2Error - then typeError $ NonFatalErrors [tcwarn] - else stTCWarnings %= add w' tcwarn + if wmode ^. warn2Error && warningName w' `elem` wmode ^. warningSet + then pure (Just tcwarn) + else Nothing <$ (stTCWarnings %= add w' tcwarn) + let errs = catMaybes merrs + unless (null errs) $ typeError $ NonFatalErrors errs + {-# SPECIALIZE warning :: Warning -> TCM () #-} warning :: MonadTCM tcm => Warning -> tcm () warning = warnings . pure @@ -82,41 +88,13 @@ deriving (Eq, Ord) isUnsolvedWarning :: Warning -> Bool -isUnsolvedWarning w = case w of - UnsolvedMetaVariables{} -> True - UnsolvedInteractionMetas{} -> True - UnsolvedConstraints{} -> True - -- rest - _ -> False +isUnsolvedWarning w = warningName w `elem` unsolvedWarnings classifyWarning :: Warning -> WhichWarnings -classifyWarning w = case w of - OldBuiltin{} -> AllWarnings - EmptyRewritePragma -> AllWarnings - UselessPublic -> AllWarnings - UnreachableClauses{} -> AllWarnings - UselessInline{} -> AllWarnings - GenericWarning{} -> AllWarnings - DeprecationWarning{} -> AllWarnings - NicifierIssue{} -> AllWarnings - InversionDepthReached{} -> AllWarnings - UserWarning{} -> AllWarnings - TerminationIssue{} -> ErrorWarnings - CoverageIssue{} -> ErrorWarnings - CoverageNoExactSplit{} -> ErrorWarnings - NotStrictlyPositive{} -> ErrorWarnings - UnsolvedMetaVariables{} -> ErrorWarnings - UnsolvedInteractionMetas{} -> ErrorWarnings - UnsolvedConstraints{} -> ErrorWarnings - GenericNonFatalError{} -> ErrorWarnings - SafeFlagPostulate{} -> ErrorWarnings - SafeFlagPragma{} -> ErrorWarnings - SafeFlagNonTerminating -> ErrorWarnings - SafeFlagTerminating -> ErrorWarnings - SafeFlagPrimTrustMe -> ErrorWarnings - SafeFlagNoPositivityCheck -> ErrorWarnings - SafeFlagPolarity -> ErrorWarnings - ParseWarning{} -> ErrorWarnings +classifyWarning w = + if warningName w `elem` errorWarnings + then ErrorWarnings + else AllWarnings -- | Should we only emit a single warning with this constructor. onlyOnce :: Warning -> Bool diff --git a/stack-7.10.3.yaml b/stack-7.10.3.yaml --- a/stack-7.10.3.yaml +++ b/stack-7.10.3.yaml @@ -1,3 +1,6 @@ +# The version installed of `cpphs` should match the lower version +# required in Agda.cabal [Issue #2315]. + resolver: lts-6.35 extra-deps: @@ -6,6 +9,7 @@ - equivalence-0.3.2 - async-2.2.1 - gitrev-1.3.1 +- text-1.2.3.1 # Local packages, usually specified by relative directory name packages: diff --git a/stack-8.0.2.yaml b/stack-8.0.2.yaml --- a/stack-8.0.2.yaml +++ b/stack-8.0.2.yaml @@ -2,6 +2,7 @@ extra-deps: - async-2.2.1 +- text-1.2.3.1 # Local packages, usually specified by relative directory name packages: diff --git a/stack-8.2.2.yaml b/stack-8.2.2.yaml --- a/stack-8.2.2.yaml +++ b/stack-8.2.2.yaml @@ -1,7 +1,8 @@ -resolver: lts-11.11 +resolver: lts-11.22 extra-deps: - async-2.2.1 +- text-1.2.3.1 # Local packages, usually specified by relative directory name packages: diff --git a/stack-8.4.3.yaml b/stack-8.4.3.yaml deleted file mode 100644 --- a/stack-8.4.3.yaml +++ /dev/null @@ -1,5 +0,0 @@ -resolver: lts-12.0 - -# Local packages, usually specified by relative directory name -packages: -- '.' diff --git a/stack-8.4.4.yaml b/stack-8.4.4.yaml new file mode 100644 --- /dev/null +++ b/stack-8.4.4.yaml @@ -0,0 +1,5 @@ +resolver: lts-12.16 + +# Local packages, usually specified by relative directory name +packages: +- '.'