search

commercialhaskell / stack

The Haskell Tool Stack
http://haskellstack.org
BSD 3-Clause "New" or "Revised" License
4k stars 843 forks source link

Agda build failure with cpphs and GHC 9.4.5 on Windows #6111

Closed andreasabel closed 1 year ago

andreasabel commented 1 year ago

When upgrading the stack CI on Windows of Agda from GHC 9.4.4 (Choco installed) to 9.4.5 (ghcup installed), I encounter problems with the stack build if using cpphs instead of the standard CPP. https://github.com/agda/agda/actions/runs/4823267306/jobs/8591538301

Agda       > Building library for Agda-2.6.4..
Agda       > 
Agda       > C:\Users\RUNNER~1\AppData\Local\Temp\ghc5396_0\ghc_25.hscpp:1:7: error:
Agda       >     lexical error in pragma at character '1'
Agda       >   |
Agda       > 1 | #line 1 ".stack-work           
...

Any clue how to fix this?

hasufell commented 1 year ago

Have you tried with choco installed 9.4.5?

andreasabel commented 1 year ago

Have you tried with choco installed 9.4.5?

No, 9.4.5 is not out yet with choco: https://community.chocolatey.org/packages/ghc#versionhistory

andreasabel commented 1 year ago

I have seen the same problem before:

Ah, ok, a similar symptom: https://github.com/agda/agda/actions/runs/4823267306/jobs/8591538301#step:10:14

WARNING: Ignoring ansi-terminal's bounds on Win32 (>=2.13.1); using Win32-2.12.0.1.

So looking at ansi-terminal: https://github.com/UnkindPartition/ansi-terminal/blob/2a4a6d89980801ae353fb573753d6205f90115e7/ansi-terminal/ansi-terminal.cabal#L53-L56

                if flag(Win32-2-13-1)
                      Build-Depends:   Win32 >= 2.13.1
                else
                      Build-Depends:   Win32 < 2.13.1, mintty

It seems that it is not safe to ignore the bound on Win32, because that would require to add mintty as a dependency.

This is where I reported the problem the last time:

Now I filed a PR to stackage:

andreasabel commented 1 year ago

Unfortunately, fixing the flag setting for ansi-terminal did not fix the problem: The warning has disappeared: https://github.com/agda/agda/actions/runs/4827829386/jobs/8600964097#step:10:14 But the error remains: https://github.com/agda/agda/actions/runs/4827829386/jobs/8600964097#step:12:25

Agda       > C:\Users\RUNNER~1\AppData\Local\Temp\ghc1952_0\ghc_25.hscpp:1:7: error:
Agda       >     lexical error in pragma at character '1'
Agda       >   |
Agda       > 1 | #line 1 ".stack-work

I can reproduce the problem on a local Window 10 machine with

I cannot reproduce the problem with a stack-installed ghc. Thus, I conclude something must be going wrong with the ghcup install of ghc-9.4 on Windows. @hasufell : Shall I report this to the ghcup issue tracker?

andreasabel commented 1 year ago

Reported to ghcup:

@hasufell wrote:

Have you tried with choco installed 9.4.5?

Since it is not 9.4.5 specific, and older choco-installed ghcs work fine, I think I can exclude this avenue.

hasufell commented 1 year ago

Is this error produced by GHC itself or alex/happy?

andreasabel commented 1 year ago

Is this error produced by GHC itself or alex/happy?

Good question, let me try to find out.

andreasabel commented 1 year ago

It is GHC:

"C:\ghcup\bin\ghc-9.4.5.exe" "--make" "-fbuilding-cabal-package" "-O" "-outputdir" ".stack-work\dist\22605e11\build" "-odir" ".stack-work\dist\22605e11\build" "-hidir" ".stack-work\dist\22605e11\build" "-stubdir" ".stack-work\dist\22605e11\build" "-i" "-i.stack-work\dist\22605e11\build" "-isrc/full" "-i.stack-work\dist\22605e11\build\autogen" "-i.stack-work\dist\22605e11\build\global-autogen" "-I.stack-work\dist\22605e11\build\autogen" "-I.stack-work\dist\22605e11\build\global-autogen" "-I.stack-work\dist\22605e11\build" "-IC:\Users\abel\AppData\Local\Programs\stack\x86_64-windows\msys2-20180531\mingw64\include" "-optP-include" "-optP.stack-work\dist\22605e11\build\autogen\cabal_macros.h" "-this-unit-id" "Agda-2.6.4-Fkdn7KRq8MBIh696A5axtH" "-hide-all-packages" "-Wmissing-home-modules" "-no-user-package-db" "-package-db" "C:\sr\snapshots\d8029e62\pkgdb" "-package-db" "C:\Users\abel\agda\.stack-work\install\269a8ba3\pkgdb" "-package-db" ".stack-work\dist\22605e11\package.conf.inplace" "-package-id" "STMonadTrans-0.4.6-7bJSgKwM2s0BRJPH6LqGQa" "-package-id" "Win32-2.12.0.1" "-package-id" "aeson-2.1.2.1-7xPKIpNDmt64JuLtenj3eV" "-package-id" "array-0.5.4.0" "-package-id" "async-2.2.4-3ME05dHmEBrDnRTVFSvcGc" "-package-id" "base-4.17.1.0" "-package-id" "binary-0.8.9.1" "-package-id" "blaze-html-0.9.1.2-38lyFDueaN76YOL6QIMVAR" "-package-id" "boxes-0.1.5-X7NROQ9QQGstZgW1GEtN" "-package-id" "bytestring-0.11.4.0" "-package-id" "case-insensitive-1.2.1.0-3kxnrIvc1hl23FrcOtEeHB" "-package-id" "containers-0.6.7" "-package-id" "data-hash-0.2.0.1-9smVPZed7tqDDTpLGJ1dUm" "-package-id" "deepseq-1.4.8.0" "-package-id" "directory-1.3.7.1" "-package-id" "dlist-1.0-JzOWexo5YFr69Ecc5W9Clo" "-package-id" "edit-distance-0.2.2.1-Fc0Uo3oQYUw9aJQDfMocrE" "-package-id" "equivalence-0.4.1-EBAhTTvhIlX4NZiISxCsvX" "-package-id" "exceptions-0.10.5" "-package-id" "filepath-1.4.2.2" "-package-id" "ghc-compact-0.1.0.0" "-package-id" "gitrev-1.3.1-BEWU3G4ST7fDqZ4Vr45DEm" "-package-id" "hashable-1.4.2.0-GSowZAAqge792LlNNo7CcE" "-package-id" "haskeline-0.8.2.1-8oiEvLsfY99ZWbxWlVZNI" "-package-id" "monad-control-1.0.3.1-IjxEDzziPCaDWgW2K8GLAI" "-package-id" "mtl-2.2.2" "-package-id" "murmur-hash-0.1.0.10-CqHLzhKRYyJCrMJ8DaEneV" "-package-id" "parallel-3.2.2.0-36KAHtmQlbB59K6tPbQ0Jr" "-package-id" "peano-0.1.0.1-E1x4HJNPjec5R7MZLdA6hH" "-package-id" "pretty-1.1.3.6" "-package-id" "process-1.6.16.0" "-package-id" "regex-tdfa-1.3.2-LLomkmblGgXI16vCr38oCv" "-package-id" "split-0.2.3.5-u3oGLAiW7JJbxIffWSCWf" "-package-id" "stm-2.5.1.0" "-package-id" "strict-0.4.0.1-8iZm2tuLdx3H7nfqcGDPd2" "-package-id" "text-2.0.2" "-package-id" "time-1.12.2" "-package-id" "time-compat-1.9.6.1-EdMANfqCkV5VHEI1N64Ju" "-package-id" "transformers-0.5.6.2" "-package-id" "unordered-containers-0.2.19.1-3vgeKBWOEKa2LoZ9GjinL2" "-package-id" "uri-encode-1.5.0.7-HQshPjzAt1vLY7sRI9ulvj" "-package-id" "vector-0.12.3.1-J1fTZdmAv2S8fMgFH7ntcO" "-package-id" "vector-hashtables-0.1.1.3-BhchOV4qcZ5Jxl3DP5GC2Q" "-package-id" "zlib-0.6.3.0-6pdOcU0xw6kFuchaK75o9o" "-XHaskell2010" "-XBangPatterns" "-XConstraintKinds" "-XDefaultSignatures" "-XDeriveFoldable" "-XDeriveFunctor" "-XDeriveGeneric" "-XDeriveTraversable" "-XExistentialQuantification" "-XFlexibleContexts" "-XFlexibleInstances" "-XFunctionalDependencies" "-XGeneralizedNewtypeDeriving" "-XInstanceSigs" "-XLambdaCase" "-XMultiParamTypeClasses" "-XMultiWayIf" "-XNamedFieldPuns" "-XOverloadedStrings" "-XPatternSynonyms" "-XRankNTypes" "-XRecordWildCards" "-XScopedTypeVariables" "-XStandaloneDeriving" "-XTupleSections" "-XTypeFamilies" "-XTypeOperators" "-XTypeSynonymInstances" "Agda.Auto.Auto" "Agda.Auto.Options" "Agda.Auto.CaseSplit" "Agda.Auto.Convert" "Agda.Auto.NarrowingSearch" "Agda.Auto.SearchControl" "Agda.Auto.Syntax" "Agda.Auto.Typecheck" "Agda.Benchmarking" "Agda.Compiler.Backend" "Agda.Compiler.Builtin" "Agda.Compiler.CallCompiler" "Agda.Compiler.Common" "Agda.Compiler.JS.Compiler" "Agda.Compiler.JS.Syntax" "Agda.Compiler.JS.Substitution" "Agda.Compiler.JS.Pretty" "Agda.Compiler.MAlonzo.Coerce" "Agda.Compiler.MAlonzo.Compiler" "Agda.Compiler.MAlonzo.Encode" "Agda.Compiler.MAlonzo.HaskellTypes" "Agda.Compiler.MAlonzo.Misc" "Agda.Compiler.MAlonzo.Pragmas" "Agda.Compiler.MAlonzo.Pretty" "Agda.Compiler.MAlonzo.Primitives" "Agda.Compiler.MAlonzo.Strict" "Agda.Compiler.ToTreeless" "Agda.Compiler.Treeless.AsPatterns" "Agda.Compiler.Treeless.Builtin" "Agda.Compiler.Treeless.Compare" "Agda.Compiler.Treeless.EliminateDefaults" "Agda.Compiler.Treeless.EliminateLiteralPatterns" "Agda.Compiler.Treeless.Erase" "Agda.Compiler.Treeless.GuardsToPrims" "Agda.Compiler.Treeless.Identity" "Agda.Compiler.Treeless.NormalizeNames" "Agda.Compiler.Treeless.Pretty" "Agda.Compiler.Treeless.Simplify" "Agda.Compiler.Treeless.Subst" "Agda.Compiler.Treeless.Uncase" "Agda.Compiler.Treeless.Unused" "Agda.ImpossibleTest" "Agda.Interaction.AgdaTop" "Agda.Interaction.Base" "Agda.Interaction.BasicOps" "Agda.Interaction.SearchAbout" "Agda.Interaction.CommandLine" "Agda.Interaction.EmacsCommand" "Agda.Interaction.EmacsTop" "Agda.Interaction.ExitCode" "Agda.Interaction.JSONTop" "Agda.Interaction.JSON" "Agda.Interaction.FindFile" "Agda.Interaction.Highlighting.Common" "Agda.Interaction.Highlighting.Dot" "Agda.Interaction.Highlighting.Emacs" "Agda.Interaction.Highlighting.FromAbstract" "Agda.Interaction.Highlighting.Generate" "Agda.Interaction.Highlighting.HTML" "Agda.Interaction.Highlighting.JSON" "Agda.Interaction.Highlighting.Precise" "Agda.Interaction.Highlighting.Range" "Agda.Interaction.Highlighting.Vim" "Agda.Interaction.Highlighting.LaTeX" "Agda.Interaction.Imports" "Agda.Interaction.InteractionTop" "Agda.Interaction.Response" "Agda.Interaction.MakeCase" "Agda.Interaction.Monad" "Agda.Interaction.Library" "Agda.Interaction.Library.Base" "Agda.Interaction.Library.Parse" "Agda.Interaction.Options" "Agda.Interaction.Options.Help" "Agda.Interaction.Options.Lenses" "Agda.Interaction.Options.Warnings" "Agda.Main" "Agda.Syntax.Abstract.Name" "Agda.Syntax.Abstract.Pattern" "Agda.Syntax.Abstract.PatternSynonyms" "Agda.Syntax.Abstract.Pretty" "Agda.Syntax.Abstract.UsedNames" "Agda.Syntax.Abstract.Views" "Agda.Syntax.Abstract" "Agda.Syntax.Builtin" "Agda.Syntax.Common" "Agda.Syntax.Concrete.Attribute" "Agda.Syntax.Concrete.Definitions" "Agda.Syntax.Concrete.Definitions.Errors" "Agda.Syntax.Concrete.Definitions.Monad" "Agda.Syntax.Concrete.Definitions.Types" "Agda.Syntax.Concrete.Fixity" "Agda.Syntax.Concrete.Generic" "Agda.Syntax.Concrete.Glyph" "Agda.Syntax.Concrete.Name" "Agda.Syntax.Concrete.Operators.Parser" "Agda.Syntax.Concrete.Operators.Parser.Monad" "Agda.Syntax.Concrete.Operators" "Agda.Syntax.Concrete.Pattern" "Agda.Syntax.Concrete.Pretty" "Agda.Syntax.Concrete" "Agda.Syntax.DoNotation" "Agda.Syntax.Fixity" "Agda.Syntax.IdiomBrackets" "Agda.Syntax.Info" "Agda.Syntax.Internal" "Agda.Syntax.Internal.Blockers" "Agda.Syntax.Internal.Defs" "Agda.Syntax.Internal.Elim" "Agda.Syntax.Internal.Generic" "Agda.Syntax.Internal.MetaVars" "Agda.Syntax.Internal.Names" "Agda.Syntax.Internal.Pattern" "Agda.Syntax.Internal.SanityCheck" "Agda.Syntax.Literal" "Agda.Syntax.Notation" "Agda.Syntax.Parser.Alex" "Agda.Syntax.Parser.Comments" "Agda.Syntax.Parser.Layout" "Agda.Syntax.Parser.LexActions" "Agda.Syntax.Parser.Lexer" "Agda.Syntax.Parser.Literate" "Agda.Syntax.Parser.LookAhead" "Agda.Syntax.Parser.Monad" "Agda.Syntax.Parser.Parser" "Agda.Syntax.Parser.StringLiterals" "Agda.Syntax.Parser.Tokens" "Agda.Syntax.Parser" "Agda.Syntax.Position" "Agda.Syntax.Reflected" "Agda.Syntax.Scope.Base" "Agda.Syntax.Scope.Flat" "Agda.Syntax.Scope.Monad" "Agda.Syntax.TopLevelModuleName" "Agda.Syntax.Translation.AbstractToConcrete" "Agda.Syntax.Translation.ConcreteToAbstract" "Agda.Syntax.Translation.InternalToAbstract" "Agda.Syntax.Translation.ReflectedToAbstract" "Agda.Syntax.Treeless" "Agda.Termination.CallGraph" "Agda.Termination.CallMatrix" "Agda.Termination.CutOff" "Agda.Termination.Monad" "Agda.Termination.Order" "Agda.Termination.RecCheck" "Agda.Termination.SparseMatrix" "Agda.Termination.Semiring" "Agda.Termination.TermCheck" "Agda.Termination.Termination" "Agda.TheTypeChecker" "Agda.TypeChecking.Abstract" "Agda.TypeChecking.CheckInternal" "Agda.TypeChecking.CompiledClause" "Agda.TypeChecking.CompiledClause.Compile" "Agda.TypeChecking.CompiledClause.Match" "Agda.TypeChecking.Constraints" "Agda.TypeChecking.Conversion" "Agda.TypeChecking.Conversion.Pure" "Agda.TypeChecking.Coverage" "Agda.TypeChecking.Coverage.Match" "Agda.TypeChecking.Coverage.SplitTree" "Agda.TypeChecking.Coverage.SplitClause" "Agda.TypeChecking.Coverage.Cubical" "Agda.TypeChecking.Datatypes" "Agda.TypeChecking.DeadCode" "Agda.TypeChecking.DisplayForm" "Agda.TypeChecking.DropArgs" "Agda.TypeChecking.Empty" "Agda.TypeChecking.EtaContract" "Agda.TypeChecking.EtaExpand" "Agda.TypeChecking.Errors" "Agda.TypeChecking.Free" "Agda.TypeChecking.Free.Lazy" "Agda.TypeChecking.Free.Precompute" "Agda.TypeChecking.Free.Reduce" "Agda.TypeChecking.Forcing" "Agda.TypeChecking.Functions" "Agda.TypeChecking.Generalize" "Agda.TypeChecking.IApplyConfluence" "Agda.TypeChecking.Implicit" "Agda.TypeChecking.Injectivity" "Agda.TypeChecking.Inlining" "Agda.TypeChecking.InstanceArguments" "Agda.TypeChecking.Irrelevance" "Agda.TypeChecking.Level" "Agda.TypeChecking.LevelConstraints" "Agda.TypeChecking.Lock" "Agda.TypeChecking.Level.Solve" "Agda.TypeChecking.MetaVars" "Agda.TypeChecking.MetaVars.Mention" "Agda.TypeChecking.MetaVars.Occurs" "Agda.TypeChecking.Monad.Base" "Agda.TypeChecking.Monad.Benchmark" "Agda.TypeChecking.Monad.Builtin" "Agda.TypeChecking.Monad.Caching" "Agda.TypeChecking.Monad.Closure" "Agda.TypeChecking.Monad.Constraints" "Agda.TypeChecking.Monad.Context" "Agda.TypeChecking.Monad.Debug" "Agda.TypeChecking.Monad.Env" "Agda.TypeChecking.Monad.Imports" "Agda.TypeChecking.Monad.MetaVars" "Agda.TypeChecking.Monad.Mutual" "Agda.TypeChecking.Monad.Open" "Agda.TypeChecking.Monad.Options" "Agda.TypeChecking.Monad.Pure" "Agda.TypeChecking.Monad.Signature" "Agda.TypeChecking.Monad.SizedTypes" "Agda.TypeChecking.Monad.State" "Agda.TypeChecking.Monad.Statistics" "Agda.TypeChecking.Monad.Trace" "Agda.TypeChecking.Monad" "Agda.TypeChecking.Names" "Agda.TypeChecking.Patterns.Abstract" "Agda.TypeChecking.Patterns.Internal" "Agda.TypeChecking.Patterns.Match" "Agda.TypeChecking.Polarity" "Agda.TypeChecking.Positivity" "Agda.TypeChecking.Positivity.Occurrence" "Agda.TypeChecking.Pretty" "Agda.TypeChecking.Pretty.Call" "Agda.TypeChecking.Pretty.Constraint" "Agda.TypeChecking.Pretty.Warning" "Agda.TypeChecking.Primitive" "Agda.TypeChecking.Primitive.Base" "Agda.TypeChecking.Primitive.Cubical" "Agda.TypeChecking.Primitive.Cubical.Id" "Agda.TypeChecking.Primitive.Cubical.Glue" "Agda.TypeChecking.Primitive.Cubical.Base" "Agda.TypeChecking.Primitive.Cubical.HCompU" "Agda.TypeChecking.ProjectionLike" "Agda.TypeChecking.Quote" "Agda.TypeChecking.ReconstructParameters" "Agda.TypeChecking.RecordPatterns" "Agda.TypeChecking.Records" "Agda.TypeChecking.Reduce" "Agda.TypeChecking.Reduce.Fast" "Agda.TypeChecking.Reduce.Monad" "Agda.TypeChecking.Rewriting" "Agda.TypeChecking.Rewriting.Clause" "Agda.TypeChecking.Rewriting.Confluence" "Agda.TypeChecking.Rewriting.NonLinMatch" "Agda.TypeChecking.Rewriting.NonLinPattern" "Agda.TypeChecking.Rules.Application" "Agda.TypeChecking.Rules.Builtin" "Agda.TypeChecking.Rules.Builtin.Coinduction" "Agda.TypeChecking.Rules.Data" "Agda.TypeChecking.Rules.Decl" "Agda.TypeChecking.Rules.Def" "Agda.TypeChecking.Rules.Display" "Agda.TypeChecking.Rules.LHS" "Agda.TypeChecking.Rules.LHS.Implicit" "Agda.TypeChecking.Rules.LHS.Problem" "Agda.TypeChecking.Rules.LHS.ProblemRest" "Agda.TypeChecking.Rules.LHS.Unify" "Agda.TypeChecking.Rules.LHS.Unify.Types" "Agda.TypeChecking.Rules.LHS.Unify.LeftInverse" "Agda.TypeChecking.Rules.Record" "Agda.TypeChecking.Rules.Term" "Agda.TypeChecking.Serialise" "Agda.TypeChecking.Serialise.Base" "Agda.TypeChecking.Serialise.Instances" "Agda.TypeChecking.Serialise.Instances.Abstract" "Agda.TypeChecking.Serialise.Instances.Common" "Agda.TypeChecking.Serialise.Instances.Compilers" "Agda.TypeChecking.Serialise.Instances.Highlighting" "Agda.TypeChecking.Serialise.Instances.Internal" "Agda.TypeChecking.Serialise.Instances.Errors" "Agda.TypeChecking.SizedTypes" "Agda.TypeChecking.SizedTypes.Solve" "Agda.TypeChecking.SizedTypes.Syntax" "Agda.TypeChecking.SizedTypes.Utils" "Agda.TypeChecking.SizedTypes.WarshallSolver" "Agda.TypeChecking.Sort" "Agda.TypeChecking.Substitute" "Agda.TypeChecking.Substitute.Class" "Agda.TypeChecking.Substitute.DeBruijn" "Agda.TypeChecking.SyntacticEquality" "Agda.TypeChecking.Telescope" "Agda.TypeChecking.Telescope.Path" "Agda.TypeChecking.Unquote" "Agda.TypeChecking.Warnings" "Agda.TypeChecking.With" "Agda.Utils.AffineHole" "Agda.Utils.Applicative" "Agda.Utils.AssocList" "Agda.Utils.Bag" "Agda.Utils.Benchmark" "Agda.Utils.BiMap" "Agda.Utils.BoolSet" "Agda.Utils.CallStack" "Agda.Utils.Char" "Agda.Utils.Cluster" "Agda.Utils.Empty" "Agda.Utils.Environment" "Agda.Utils.Either" "Agda.Utils.Fail" "Agda.Utils.Favorites" "Agda.Utils.FileName" "Agda.Utils.Float" "Agda.Utils.Functor" "Agda.Utils.Function" "Agda.Utils.Graph.AdjacencyMap.Unidirectional" "Agda.Utils.Graph.TopSort" "Agda.Utils.Hash" "Agda.Utils.HashTable" "Agda.Utils.Haskell.Syntax" "Agda.Utils.Impossible" "Agda.Utils.IndexedList" "Agda.Utils.IntSet.Infinite" "Agda.Utils.IO" "Agda.Utils.IO.Binary" "Agda.Utils.IO.Directory" "Agda.Utils.IO.TempFile" "Agda.Utils.IO.UTF8" "Agda.Utils.IORef" "Agda.Utils.Lens" "Agda.Utils.Lens.Examples" "Agda.Utils.List" "Agda.Utils.List1" "Agda.Utils.List2" "Agda.Utils.ListT" "Agda.Utils.Map" "Agda.Utils.Maybe" "Agda.Utils.Maybe.Strict" "Agda.Utils.Memo" "Agda.Utils.Monad" "Agda.Utils.Monoid" "Agda.Utils.Null" "Agda.Utils.Parser.MemoisedCPS" "Agda.Utils.PartialOrd" "Agda.Utils.Permutation" "Agda.Utils.Pointer" "Agda.Utils.POMonoid" "Agda.Utils.Pretty" "Agda.Utils.ProfileOptions" "Agda.Utils.RangeMap" "Agda.Utils.SemiRing" "Agda.Utils.Semigroup" "Agda.Utils.Singleton" "Agda.Utils.Size" "Agda.Utils.SmallSet" "Agda.Utils.String" "Agda.Utils.Suffix" "Agda.Utils.Three" "Agda.Utils.Time" "Agda.Utils.Trie" "Agda.Utils.Tuple" "Agda.Utils.TypeLevel" "Agda.Utils.TypeLits" "Agda.Utils.Update" "Agda.Utils.VarSet" "Agda.Utils.Warshall" "Agda.Utils.WithDefault" "Agda.Utils.Zipper" "Agda.Version" "Agda.VersionCommit" "Paths_Agda" "Agda.Interaction.Highlighting.Dot.Backend" "Agda.Interaction.Highlighting.Dot.Base" "Agda.Interaction.Highlighting.HTML.Backend" "Agda.Interaction.Highlighting.HTML.Base" "Agda.Interaction.Highlighting.LaTeX.Backend" "Agda.Interaction.Highlighting.LaTeX.Base" "Agda.Interaction.Options.Base" "Agda.Interaction.Options.HasOptions" "Agda.Utils.CallStack.Base" "Agda.Utils.CallStack.Pretty" "-fprint-potential-instances" "-Werror" "-Werror=cpp-undef" "-Werror=deprecated-flags" "-Werror=deriving-typeable" "-Werror=dodgy-exports" "-Werror=dodgy-foreign-imports" "-Werror=dodgy-imports" "-Werror=duplicate-exports" "-Werror=empty-enumerations" "-Werror=identities" "-Werror=inaccessible-code" "-Werror=inline-rule-shadowing" "-Werror=missing-fields" "-Werror=missing-home-modules" "-Werror=missing-methods" "-Werror=missing-pattern-synonym-signatures" "-Werror=missing-signatures" "-Werror=noncanonical-monad-instances" "-Werror=noncanonical-monoid-instances" "-Werror=overflowed-literals" "-Werror=overlapping-patterns" "-Werror=semigroup" "-Werror=simplifiable-class-constraints" "-Werror=star-binder" "-Werror=star-is-type" "-Werror=tabs" "-Werror=typed-holes" "-Werror=unbanged-strict-patterns" "-Werror=unrecognised-pragmas" "-Werror=unrecognised-warning-flags" "-Werror=unticked-promoted-constructors" "-Werror=unused-do-bind" "-Werror=unused-foralls" "-Werror=warnings-deprecations" "-Werror=wrong-do-bind" "-Werror=missed-extra-shared-lib" "-Werror=compat-unqualified-imports" "-Werror=deriving-defaults" "-Werror=redundant-record-wildcards" "-Werror=unused-packages" "-Werror=unused-record-wildcards" "-Werror=invalid-haddock" "-Werror=incomplete-patterns" "-Werror=incomplete-record-updates" "-Werror=unicode-bidirectional-format-characters" "-Werror=redundant-bang-patterns" "-Werror=forall-identifier" "-Werror=type-equality-out-of-scope" "-pgmP" "cpphs" "-optP" "--cpp" "-O0" "-fhide-source-paths" "-fdiagnostics-color=always"
"C:\ghcup\bin\ghc-9.4.5.exe" \ "--make" \ "-fbuilding-cabal-package" \ "-O" \ "-outputdir" \ ".stack-work\dist\22605e11\build" \ "-odir" \ ".stack-work\dist\22605e11\build" \ "-hidir" \ ".stack-work\dist\22605e11\build" \ "-stubdir" \ ".stack-work\dist\22605e11\build" \ "-i" \ "-i.stack-work\dist\22605e11\build" \ "-isrc/full" \ "-i.stack-work\dist\22605e11\build\autogen" \ "-i.stack-work\dist\22605e11\build\global-autogen" \ "-I.stack-work\dist\22605e11\build\autogen" \ "-I.stack-work\dist\22605e11\build\global-autogen" \ "-I.stack-work\dist\22605e11\build" \ "-IC:\Users\abel\AppData\Local\Programs\stack\x86_64-windows\msys2-20180531\mingw64\include" \ "-optP-include" \ "-optP.stack-work\dist\22605e11\build\autogen\cabal_macros.h" \ "-this-unit-id" \ "Agda-2.6.4-Fkdn7KRq8MBIh696A5axtH" \ "-hide-all-packages" \ "-Wmissing-home-modules" \ "-no-user-package-db" \ "-package-db" \ "C:\sr\snapshots\d8029e62\pkgdb" \ "-package-db" \ "C:\Users\abel\agda\.stack-work\install\269a8ba3\pkgdb" \ "-package-db" \ ".stack-work\dist\22605e11\package.conf.inplace" \ "-package-id" \ "STMonadTrans-0.4.6-7bJSgKwM2s0BRJPH6LqGQa" \ "-package-id" \ "Win32-2.12.0.1" \ "-package-id" \ "aeson-2.1.2.1-7xPKIpNDmt64JuLtenj3eV" \ "-package-id" \ "array-0.5.4.0" \ "-package-id" \ "async-2.2.4-3ME05dHmEBrDnRTVFSvcGc" \ "-package-id" \ "base-4.17.1.0" \ "-package-id" \ "binary-0.8.9.1" \ "-package-id" \ "blaze-html-0.9.1.2-38lyFDueaN76YOL6QIMVAR" \ "-package-id" \ "boxes-0.1.5-X7NROQ9QQGstZgW1GEtN" \ "-package-id" \ "bytestring-0.11.4.0" \ "-package-id" \ "case-insensitive-1.2.1.0-3kxnrIvc1hl23FrcOtEeHB" \ "-package-id" \ "containers-0.6.7" \ "-package-id" \ "data-hash-0.2.0.1-9smVPZed7tqDDTpLGJ1dUm" \ "-package-id" \ "deepseq-1.4.8.0" \ "-package-id" \ "directory-1.3.7.1" \ "-package-id" \ "dlist-1.0-JzOWexo5YFr69Ecc5W9Clo" \ "-package-id" \ "edit-distance-0.2.2.1-Fc0Uo3oQYUw9aJQDfMocrE" \ "-package-id" \ "equivalence-0.4.1-EBAhTTvhIlX4NZiISxCsvX" \ "-package-id" \ "exceptions-0.10.5" \ "-package-id" \ "filepath-1.4.2.2" \ "-package-id" \ "ghc-compact-0.1.0.0" \ "-package-id" \ "gitrev-1.3.1-BEWU3G4ST7fDqZ4Vr45DEm" \ "-package-id" \ "hashable-1.4.2.0-GSowZAAqge792LlNNo7CcE" \ "-package-id" \ "haskeline-0.8.2.1-8oiEvLsfY99ZWbxWlVZNI" \ "-package-id" \ "monad-control-1.0.3.1-IjxEDzziPCaDWgW2K8GLAI" \ "-package-id" \ "mtl-2.2.2" \ "-package-id" \ "murmur-hash-0.1.0.10-CqHLzhKRYyJCrMJ8DaEneV" \ "-package-id" \ "parallel-3.2.2.0-36KAHtmQlbB59K6tPbQ0Jr" \ "-package-id" \ "peano-0.1.0.1-E1x4HJNPjec5R7MZLdA6hH" \ "-package-id" \ "pretty-1.1.3.6" \ "-package-id" \ "process-1.6.16.0" \ "-package-id" \ "regex-tdfa-1.3.2-LLomkmblGgXI16vCr38oCv" \ "-package-id" \ "split-0.2.3.5-u3oGLAiW7JJbxIffWSCWf" \ "-package-id" \ "stm-2.5.1.0" \ "-package-id" \ "strict-0.4.0.1-8iZm2tuLdx3H7nfqcGDPd2" \ "-package-id" \ "text-2.0.2" \ "-package-id" \ "time-1.12.2" \ "-package-id" \ "time-compat-1.9.6.1-EdMANfqCkV5VHEI1N64Ju" \ "-package-id" \ "transformers-0.5.6.2" \ "-package-id" \ "unordered-containers-0.2.19.1-3vgeKBWOEKa2LoZ9GjinL2" \ "-package-id" \ "uri-encode-1.5.0.7-HQshPjzAt1vLY7sRI9ulvj" \ "-package-id" \ "vector-0.12.3.1-J1fTZdmAv2S8fMgFH7ntcO" \ "-package-id" \ "vector-hashtables-0.1.1.3-BhchOV4qcZ5Jxl3DP5GC2Q" \ "-package-id" \ "zlib-0.6.3.0-6pdOcU0xw6kFuchaK75o9o" \ "-XHaskell2010" \ "-XBangPatterns" \ "-XConstraintKinds" \ "-XDefaultSignatures" \ "-XDeriveFoldable" \ "-XDeriveFunctor" \ "-XDeriveGeneric" \ "-XDeriveTraversable" \ "-XExistentialQuantification" \ "-XFlexibleContexts" \ "-XFlexibleInstances" \ "-XFunctionalDependencies" \ "-XGeneralizedNewtypeDeriving" \ "-XInstanceSigs" \ "-XLambdaCase" \ "-XMultiParamTypeClasses" \ "-XMultiWayIf" \ "-XNamedFieldPuns" \ "-XOverloadedStrings" \ "-XPatternSynonyms" \ "-XRankNTypes" \ "-XRecordWildCards" \ "-XScopedTypeVariables" \ "-XStandaloneDeriving" \ "-XTupleSections" \ "-XTypeFamilies" \ "-XTypeOperators" \ "-XTypeSynonymInstances" \ "Agda.Auto.Auto" \ "Agda.Auto.Options" \ "Agda.Auto.CaseSplit" \ "Agda.Auto.Convert" \ "Agda.Auto.NarrowingSearch" \ "Agda.Auto.SearchControl" \ "Agda.Auto.Syntax" \ "Agda.Auto.Typecheck" \ "Agda.Benchmarking" \ "Agda.Compiler.Backend" \ "Agda.Compiler.Builtin" \ "Agda.Compiler.CallCompiler" \ "Agda.Compiler.Common" \ "Agda.Compiler.JS.Compiler" \ "Agda.Compiler.JS.Syntax" \ "Agda.Compiler.JS.Substitution" \ "Agda.Compiler.JS.Pretty" \ "Agda.Compiler.MAlonzo.Coerce" \ "Agda.Compiler.MAlonzo.Compiler" \ "Agda.Compiler.MAlonzo.Encode" \ "Agda.Compiler.MAlonzo.HaskellTypes" \ "Agda.Compiler.MAlonzo.Misc" \ "Agda.Compiler.MAlonzo.Pragmas" \ "Agda.Compiler.MAlonzo.Pretty" \ "Agda.Compiler.MAlonzo.Primitives" \ "Agda.Compiler.MAlonzo.Strict" \ "Agda.Compiler.ToTreeless" \ "Agda.Compiler.Treeless.AsPatterns" \ "Agda.Compiler.Treeless.Builtin" \ "Agda.Compiler.Treeless.Compare" \ "Agda.Compiler.Treeless.EliminateDefaults" \ "Agda.Compiler.Treeless.EliminateLiteralPatterns" \ "Agda.Compiler.Treeless.Erase" \ "Agda.Compiler.Treeless.GuardsToPrims" \ "Agda.Compiler.Treeless.Identity" \ "Agda.Compiler.Treeless.NormalizeNames" \ "Agda.Compiler.Treeless.Pretty" \ "Agda.Compiler.Treeless.Simplify" \ "Agda.Compiler.Treeless.Subst" \ "Agda.Compiler.Treeless.Uncase" \ "Agda.Compiler.Treeless.Unused" \ "Agda.ImpossibleTest" \ "Agda.Interaction.AgdaTop" \ "Agda.Interaction.Base" \ "Agda.Interaction.BasicOps" \ "Agda.Interaction.SearchAbout" \ "Agda.Interaction.CommandLine" \ "Agda.Interaction.EmacsCommand" \ "Agda.Interaction.EmacsTop" \ "Agda.Interaction.ExitCode" \ "Agda.Interaction.JSONTop" \ "Agda.Interaction.JSON" \ "Agda.Interaction.FindFile" \ "Agda.Interaction.Highlighting.Common" \ "Agda.Interaction.Highlighting.Dot" \ "Agda.Interaction.Highlighting.Emacs" \ "Agda.Interaction.Highlighting.FromAbstract" \ "Agda.Interaction.Highlighting.Generate" \ "Agda.Interaction.Highlighting.HTML" \ "Agda.Interaction.Highlighting.JSON" \ "Agda.Interaction.Highlighting.Precise" \ "Agda.Interaction.Highlighting.Range" \ "Agda.Interaction.Highlighting.Vim" \ "Agda.Interaction.Highlighting.LaTeX" \ "Agda.Interaction.Imports" \ "Agda.Interaction.InteractionTop" \ "Agda.Interaction.Response" \ "Agda.Interaction.MakeCase" \ "Agda.Interaction.Monad" \ "Agda.Interaction.Library" \ "Agda.Interaction.Library.Base" \ "Agda.Interaction.Library.Parse" \ "Agda.Interaction.Options" \ "Agda.Interaction.Options.Help" \ "Agda.Interaction.Options.Lenses" \ "Agda.Interaction.Options.Warnings" \ "Agda.Main" \ "Agda.Syntax.Abstract.Name" \ "Agda.Syntax.Abstract.Pattern" \ "Agda.Syntax.Abstract.PatternSynonyms" \ "Agda.Syntax.Abstract.Pretty" \ "Agda.Syntax.Abstract.UsedNames" \ "Agda.Syntax.Abstract.Views" \ "Agda.Syntax.Abstract" \ "Agda.Syntax.Builtin" \ "Agda.Syntax.Common" \ "Agda.Syntax.Concrete.Attribute" \ "Agda.Syntax.Concrete.Definitions" \ "Agda.Syntax.Concrete.Definitions.Errors" \ "Agda.Syntax.Concrete.Definitions.Monad" \ "Agda.Syntax.Concrete.Definitions.Types" \ "Agda.Syntax.Concrete.Fixity" \ "Agda.Syntax.Concrete.Generic" \ "Agda.Syntax.Concrete.Glyph" \ "Agda.Syntax.Concrete.Name" \ "Agda.Syntax.Concrete.Operators.Parser" \ "Agda.Syntax.Concrete.Operators.Parser.Monad" \ "Agda.Syntax.Concrete.Operators" \ "Agda.Syntax.Concrete.Pattern" \ "Agda.Syntax.Concrete.Pretty" \ "Agda.Syntax.Concrete" \ "Agda.Syntax.DoNotation" \ "Agda.Syntax.Fixity" \ "Agda.Syntax.IdiomBrackets" \ "Agda.Syntax.Info" \ "Agda.Syntax.Internal" \ "Agda.Syntax.Internal.Blockers" \ "Agda.Syntax.Internal.Defs" \ "Agda.Syntax.Internal.Elim" \ "Agda.Syntax.Internal.Generic" \ "Agda.Syntax.Internal.MetaVars" \ "Agda.Syntax.Internal.Names" \ "Agda.Syntax.Internal.Pattern" \ "Agda.Syntax.Internal.SanityCheck" \ "Agda.Syntax.Literal" \ "Agda.Syntax.Notation" \ "Agda.Syntax.Parser.Alex" \ "Agda.Syntax.Parser.Comments" \ "Agda.Syntax.Parser.Layout" \ "Agda.Syntax.Parser.LexActions" \ "Agda.Syntax.Parser.Lexer" \ "Agda.Syntax.Parser.Literate" \ "Agda.Syntax.Parser.LookAhead" \ "Agda.Syntax.Parser.Monad" \ "Agda.Syntax.Parser.Parser" \ "Agda.Syntax.Parser.StringLiterals" \ "Agda.Syntax.Parser.Tokens" \ "Agda.Syntax.Parser" \ "Agda.Syntax.Position" \ "Agda.Syntax.Reflected" \ "Agda.Syntax.Scope.Base" \ "Agda.Syntax.Scope.Flat" \ "Agda.Syntax.Scope.Monad" \ "Agda.Syntax.TopLevelModuleName" \ "Agda.Syntax.Translation.AbstractToConcrete" \ "Agda.Syntax.Translation.ConcreteToAbstract" \ "Agda.Syntax.Translation.InternalToAbstract" \ "Agda.Syntax.Translation.ReflectedToAbstract" \ "Agda.Syntax.Treeless" \ "Agda.Termination.CallGraph" \ "Agda.Termination.CallMatrix" \ "Agda.Termination.CutOff" \ "Agda.Termination.Monad" \ "Agda.Termination.Order" \ "Agda.Termination.RecCheck" \ "Agda.Termination.SparseMatrix" \ "Agda.Termination.Semiring" \ "Agda.Termination.TermCheck" \ "Agda.Termination.Termination" \ "Agda.TheTypeChecker" \ "Agda.TypeChecking.Abstract" \ "Agda.TypeChecking.CheckInternal" \ "Agda.TypeChecking.CompiledClause" \ "Agda.TypeChecking.CompiledClause.Compile" \ "Agda.TypeChecking.CompiledClause.Match" \ "Agda.TypeChecking.Constraints" \ "Agda.TypeChecking.Conversion" \ "Agda.TypeChecking.Conversion.Pure" \ "Agda.TypeChecking.Coverage" \ "Agda.TypeChecking.Coverage.Match" \ "Agda.TypeChecking.Coverage.SplitTree" \ "Agda.TypeChecking.Coverage.SplitClause" \ "Agda.TypeChecking.Coverage.Cubical" \ "Agda.TypeChecking.Datatypes" \ "Agda.TypeChecking.DeadCode" \ "Agda.TypeChecking.DisplayForm" \ "Agda.TypeChecking.DropArgs" \ "Agda.TypeChecking.Empty" \ "Agda.TypeChecking.EtaContract" \ "Agda.TypeChecking.EtaExpand" \ "Agda.TypeChecking.Errors" \ "Agda.TypeChecking.Free" \ "Agda.TypeChecking.Free.Lazy" \ "Agda.TypeChecking.Free.Precompute" \ "Agda.TypeChecking.Free.Reduce" \ "Agda.TypeChecking.Forcing" \ "Agda.TypeChecking.Functions" \ "Agda.TypeChecking.Generalize" \ "Agda.TypeChecking.IApplyConfluence" \ "Agda.TypeChecking.Implicit" \ "Agda.TypeChecking.Injectivity" \ "Agda.TypeChecking.Inlining" \ "Agda.TypeChecking.InstanceArguments" \ "Agda.TypeChecking.Irrelevance" \ "Agda.TypeChecking.Level" \ "Agda.TypeChecking.LevelConstraints" \ "Agda.TypeChecking.Lock" \ "Agda.TypeChecking.Level.Solve" \ "Agda.TypeChecking.MetaVars" \ "Agda.TypeChecking.MetaVars.Mention" \ "Agda.TypeChecking.MetaVars.Occurs" \ "Agda.TypeChecking.Monad.Base" \ "Agda.TypeChecking.Monad.Benchmark" \ "Agda.TypeChecking.Monad.Builtin" \ "Agda.TypeChecking.Monad.Caching" \ "Agda.TypeChecking.Monad.Closure" \ "Agda.TypeChecking.Monad.Constraints" \ "Agda.TypeChecking.Monad.Context" \ "Agda.TypeChecking.Monad.Debug" \ "Agda.TypeChecking.Monad.Env" \ "Agda.TypeChecking.Monad.Imports" \ "Agda.TypeChecking.Monad.MetaVars" \ "Agda.TypeChecking.Monad.Mutual" \ "Agda.TypeChecking.Monad.Open" \ "Agda.TypeChecking.Monad.Options" \ "Agda.TypeChecking.Monad.Pure" \ "Agda.TypeChecking.Monad.Signature" \ "Agda.TypeChecking.Monad.SizedTypes" \ "Agda.TypeChecking.Monad.State" \ "Agda.TypeChecking.Monad.Statistics" \ "Agda.TypeChecking.Monad.Trace" \ "Agda.TypeChecking.Monad" \ "Agda.TypeChecking.Names" \ "Agda.TypeChecking.Patterns.Abstract" \ "Agda.TypeChecking.Patterns.Internal" \ "Agda.TypeChecking.Patterns.Match" \ "Agda.TypeChecking.Polarity" \ "Agda.TypeChecking.Positivity" \ "Agda.TypeChecking.Positivity.Occurrence" \ "Agda.TypeChecking.Pretty" \ "Agda.TypeChecking.Pretty.Call" \ "Agda.TypeChecking.Pretty.Constraint" \ "Agda.TypeChecking.Pretty.Warning" \ "Agda.TypeChecking.Primitive" \ "Agda.TypeChecking.Primitive.Base" \ "Agda.TypeChecking.Primitive.Cubical" \ "Agda.TypeChecking.Primitive.Cubical.Id" \ "Agda.TypeChecking.Primitive.Cubical.Glue" \ "Agda.TypeChecking.Primitive.Cubical.Base" \ "Agda.TypeChecking.Primitive.Cubical.HCompU" \ "Agda.TypeChecking.ProjectionLike" \ "Agda.TypeChecking.Quote" \ "Agda.TypeChecking.ReconstructParameters" \ "Agda.TypeChecking.RecordPatterns" \ "Agda.TypeChecking.Records" \ "Agda.TypeChecking.Reduce" \ "Agda.TypeChecking.Reduce.Fast" \ "Agda.TypeChecking.Reduce.Monad" \ "Agda.TypeChecking.Rewriting" \ "Agda.TypeChecking.Rewriting.Clause" \ "Agda.TypeChecking.Rewriting.Confluence" \ "Agda.TypeChecking.Rewriting.NonLinMatch" \ "Agda.TypeChecking.Rewriting.NonLinPattern" \ "Agda.TypeChecking.Rules.Application" \ "Agda.TypeChecking.Rules.Builtin" \ "Agda.TypeChecking.Rules.Builtin.Coinduction" \ "Agda.TypeChecking.Rules.Data" \ "Agda.TypeChecking.Rules.Decl" \ "Agda.TypeChecking.Rules.Def" \ "Agda.TypeChecking.Rules.Display" \ "Agda.TypeChecking.Rules.LHS" \ "Agda.TypeChecking.Rules.LHS.Implicit" \ "Agda.TypeChecking.Rules.LHS.Problem" \ "Agda.TypeChecking.Rules.LHS.ProblemRest" \ "Agda.TypeChecking.Rules.LHS.Unify" \ "Agda.TypeChecking.Rules.LHS.Unify.Types" \ "Agda.TypeChecking.Rules.LHS.Unify.LeftInverse" \ "Agda.TypeChecking.Rules.Record" \ "Agda.TypeChecking.Rules.Term" \ "Agda.TypeChecking.Serialise" \ "Agda.TypeChecking.Serialise.Base" \ "Agda.TypeChecking.Serialise.Instances" \ "Agda.TypeChecking.Serialise.Instances.Abstract" \ "Agda.TypeChecking.Serialise.Instances.Common" \ "Agda.TypeChecking.Serialise.Instances.Compilers" \ "Agda.TypeChecking.Serialise.Instances.Highlighting" \ "Agda.TypeChecking.Serialise.Instances.Internal" \ "Agda.TypeChecking.Serialise.Instances.Errors" \ "Agda.TypeChecking.SizedTypes" \ "Agda.TypeChecking.SizedTypes.Solve" \ "Agda.TypeChecking.SizedTypes.Syntax" \ "Agda.TypeChecking.SizedTypes.Utils" \ "Agda.TypeChecking.SizedTypes.WarshallSolver" \ "Agda.TypeChecking.Sort" \ "Agda.TypeChecking.Substitute" \ "Agda.TypeChecking.Substitute.Class" \ "Agda.TypeChecking.Substitute.DeBruijn" \ "Agda.TypeChecking.SyntacticEquality" \ "Agda.TypeChecking.Telescope" \ "Agda.TypeChecking.Telescope.Path" \ "Agda.TypeChecking.Unquote" \ "Agda.TypeChecking.Warnings" \ "Agda.TypeChecking.With" \ "Agda.Utils.AffineHole" \ "Agda.Utils.Applicative" \ "Agda.Utils.AssocList" \ "Agda.Utils.Bag" \ "Agda.Utils.Benchmark" \ "Agda.Utils.BiMap" \ "Agda.Utils.BoolSet" \ "Agda.Utils.CallStack" \ "Agda.Utils.Char" \ "Agda.Utils.Cluster" \ "Agda.Utils.Empty" \ "Agda.Utils.Environment" \ "Agda.Utils.Either" \ "Agda.Utils.Fail" \ "Agda.Utils.Favorites" \ "Agda.Utils.FileName" \ "Agda.Utils.Float" \ "Agda.Utils.Functor" \ "Agda.Utils.Function" \ "Agda.Utils.Graph.AdjacencyMap.Unidirectional" \ "Agda.Utils.Graph.TopSort" \ "Agda.Utils.Hash" \ "Agda.Utils.HashTable" \ "Agda.Utils.Haskell.Syntax" \ "Agda.Utils.Impossible" \ "Agda.Utils.IndexedList" \ "Agda.Utils.IntSet.Infinite" \ "Agda.Utils.IO" \ "Agda.Utils.IO.Binary" \ "Agda.Utils.IO.Directory" \ "Agda.Utils.IO.TempFile" \ "Agda.Utils.IO.UTF8" \ "Agda.Utils.IORef" \ "Agda.Utils.Lens" \ "Agda.Utils.Lens.Examples" \ "Agda.Utils.List" \ "Agda.Utils.List1" \ "Agda.Utils.List2" \ "Agda.Utils.ListT" \ "Agda.Utils.Map" \ "Agda.Utils.Maybe" \ "Agda.Utils.Maybe.Strict" \ "Agda.Utils.Memo" \ "Agda.Utils.Monad" \ "Agda.Utils.Monoid" \ "Agda.Utils.Null" \ "Agda.Utils.Parser.MemoisedCPS" \ "Agda.Utils.PartialOrd" \ "Agda.Utils.Permutation" \ "Agda.Utils.Pointer" \ "Agda.Utils.POMonoid" \ "Agda.Utils.Pretty" \ "Agda.Utils.ProfileOptions" \ "Agda.Utils.RangeMap" \ "Agda.Utils.SemiRing" \ "Agda.Utils.Semigroup" \ "Agda.Utils.Singleton" \ "Agda.Utils.Size" \ "Agda.Utils.SmallSet" \ "Agda.Utils.String" \ "Agda.Utils.Suffix" \ "Agda.Utils.Three" \ "Agda.Utils.Time" \ "Agda.Utils.Trie" \ "Agda.Utils.Tuple" \ "Agda.Utils.TypeLevel" \ "Agda.Utils.TypeLits" \ "Agda.Utils.Update" \ "Agda.Utils.VarSet" \ "Agda.Utils.Warshall" \ "Agda.Utils.WithDefault" \ "Agda.Utils.Zipper" \ "Agda.Version" \ "Agda.VersionCommit" \ "Paths_Agda" \ "Agda.Interaction.Highlighting.Dot.Backend" \ "Agda.Interaction.Highlighting.Dot.Base" \ "Agda.Interaction.Highlighting.HTML.Backend" \ "Agda.Interaction.Highlighting.HTML.Base" \ "Agda.Interaction.Highlighting.LaTeX.Backend" \ "Agda.Interaction.Highlighting.LaTeX.Base" \ "Agda.Interaction.Options.Base" \ "Agda.Interaction.Options.HasOptions" \ "Agda.Utils.CallStack.Base" \ "Agda.Utils.CallStack.Pretty" \ "-fprint-potential-instances" \ "-Werror" \ "-Werror=cpp-undef" \ "-Werror=deprecated-flags" \ "-Werror=deriving-typeable" \ "-Werror=dodgy-exports" \ "-Werror=dodgy-foreign-imports" \ "-Werror=dodgy-imports" \ "-Werror=duplicate-exports" \ "-Werror=empty-enumerations" \ "-Werror=identities" \ "-Werror=inaccessible-code" \ "-Werror=inline-rule-shadowing" \ "-Werror=missing-fields" \ "-Werror=missing-home-modules" \ "-Werror=missing-methods" \ "-Werror=missing-pattern-synonym-signatures" \ "-Werror=missing-signatures" \ "-Werror=noncanonical-monad-instances" \ "-Werror=noncanonical-monoid-instances" \ "-Werror=overflowed-literals" \ "-Werror=overlapping-patterns" \ "-Werror=semigroup" \ "-Werror=simplifiable-class-constraints" \ "-Werror=star-binder" \ "-Werror=star-is-type" \ "-Werror=tabs" \ "-Werror=typed-holes" \ "-Werror=unbanged-strict-patterns" \ "-Werror=unrecognised-pragmas" \ "-Werror=unrecognised-warning-flags" \ "-Werror=unticked-promoted-constructors" \ "-Werror=unused-do-bind" \ "-Werror=unused-foralls" \ "-Werror=warnings-deprecations" \ "-Werror=wrong-do-bind" \ "-Werror=missed-extra-shared-lib" \ "-Werror=compat-unqualified-imports" \ "-Werror=deriving-defaults" \ "-Werror=redundant-record-wildcards" \ "-Werror=unused-packages" \ "-Werror=unused-record-wildcards" \ "-Werror=invalid-haddock" \ "-Werror=incomplete-patterns" \ "-Werror=incomplete-record-updates" \ "-Werror=unicode-bidirectional-format-characters" \ "-Werror=redundant-bang-patterns" \ "-Werror=forall-identifier" \ "-Werror=type-equality-out-of-scope" \ "-pgmP" \ "cpphs" \ "-optP" \ "--cpp" \ ... 
"C:\ghcup\bin\ghc-9.4.5.exe" \
  "--make" \
  "-fbuilding-cabal-package" \  
  ...
  "Agda.Version" \
  "Agda.VersionCommit" \
  "Paths_Agda" \ 
  ...
  "-Werror" \
  "-Werror=cpp-undef" \
  ...
  "-pgmP" "cpphs" \
  "-optP" "--cpp" \
  ...
hasufell commented 1 year ago

https://github.com/agda/agda/issues/1285

Hmm

andreasabel commented 1 year ago

@hasufell wrote:

agda/agda#1285

Hmm

Yes, cpphs has been a headache on and off, but the issue you point to has a different error. (And has been fixed 8 years ago.)

mpilgrem commented 1 year ago

This is a puzzle, because the Stack-supplied GHC 9.4.5 and the GHCup-supplied GHC 9.4.5 should be fetching the same binary distribution on Windows (the one provided by the GHC developers).

Also, I can't reproduce the problem with the master branch of Stack:

stack --stack-yaml stack-9.4.5.yaml build --flag Agda:cpphs

works fine for me (on Windows), with Stack configuration:

resolver: nightly-2023-04-28 # GHC 9.4.5

flags:
  mintty:
    win32-2-13-1: false

extra-deps:
- vector-hashtables-0.1.1.1
hasufell commented 1 year ago

I'm guessing this is a preprocessor issue and the cpphs that's in PATH when using stack might be a different one when using cabal.

mpilgrem commented 1 year ago

The cpphs in snapshot nightly-2023-04-28 is cpphs-1.20.9.1@rev:1, which is what (I think) Stack builds and uses.

EDIT: During the build of Agda with --flag Agda:cpphs:

cpphs                        > copy/register
cpphs                        > Installing library in C:\sr\snapshots\e569656e\lib\x86_64-windows-ghc-9.4.5\cpphs-1.20.9.1-D9wTFsl7aceGEGt6HNFwvg
cpphs                        > Installing executable cpphs in C:\sr\snapshots\e569656e\bin

After a successful build of Agda with --flag Agda:cpphs, cpphs.exe is available in the Stack build environment:

stack --stack-yaml stack-9.4.5.yaml exec -- where.exe cpphs
C:\sr\snapshots\e569656e\bin\cpphs.exe
andreasabel commented 1 year ago

cpphs on Windows is a mess, see my experiments at:

All these factors contribute to success or failure:

  1. Whether using GHC 8.x or GHC 9.x
  2. Whether using cabal or stack
  3. For stack, whether to install GHC with ghcup or choco/stack.

I haven't found a setup yet that succeeds for all versions of GHC (meaning 8.10 - 9.4).

At least for Agda, I am considering to abandon cpphs:

mpilgrem commented 1 year ago

@andreasabel, I understand from your comments that the problem does not lie with Stack, but elsewhere. I am going to close this issue. If I am mistaken, please reopen it.

andreasabel commented 1 year ago

@mpilgrem : It is also a problem with Stack, e.g. for resolver lts-18.28, as witnessed here: https://github.com/hackage-trustees/malcolm-wallace-universe/actions/runs/4858876150/jobs/8660804264

Thus, I think this issue shouldn't be closed as "completed". However, I would not mind if you close it as "wont fix" (the other option how to close an issue), because I have lost interest in cpphs.

mpilgrem commented 1 year ago

@andreasabel, I can reproduce a problem on Windows with stack --stack-yaml stack-8.10.7.yaml build --flag Agda:cpphs but that does not appear to me to be a problem with Stack. Stack seems to be doing what you would expect it to do.

The output of stack --verbose --cabal-verbose --stack-yaml stack-8.10.7.yaml build --flag Agda:cpphs --ghc-options -keep-tmp-files includes:

2023-05-06 12:34:07.034646: [info] Using cpphs version 1.20.9 found on system at:
2023-05-06 12:34:07.034646: [info] C:\sr\snapshots\c3655ee5\bin\cpphs.exe
...
2023-05-06 12:34:13.049548: [warn]
2023-05-06 12:34:13.051553: [warn] C:\Users\mikep\AppData\Local\Temp\ghc28172_0\ghc_23.hscpp:1:7: error:
2023-05-06 12:34:13.051553: [warn]     lexical error in pragma at character '1'
2023-05-06 12:34:13.051553: [warn]   |
2023-05-06 12:34:13.052527: [warn] 1 | #line 1 ".stack-work
2023-05-06 12:34:13.052527: [warn]   |

The content of GHC's temporary file C:\Users\mikep\AppData\Local\Temp\ghc28172_0\ghc_23.hscpp starts:

#line 1 "src/full/Agda/Compiler/Common.hs"
#line 1 "./.stack-work

which looks to me to be malformed at line 2 (it is missing a closing ") - see https://gitlab.haskell.org/ghc/ghc/-/issues/22300 for my understanding of the valid format of a #line pragma from GHC's perspective.

It seems to me that may possibly be somehow related to this open cpphs issue: https://github.com/malcolmwallace/cpphs/issues/4

andreasabel commented 1 year ago

@mpilgrem : Thanks for the further investigation and getting closer to the problem! It is still mysterious to me how this issue surfaces or not depending on the GHC version and installation method. Oh well, I guess before there isn't any cpphs maintainer, there is little to be done about it.

mpilgrem commented 1 year ago

I've switched to simpler test code:

{-# LANGUAGE CPP #-}
module Main (main) where

main :: IO ()
main = pure ()

and

name:                boo
version:             0.1.0.0

dependencies:
- base >= 4.7 && < 5

build-tools:
- cpphs >= 1.20.9

ghc-options:
- -pgmP cpphs
- -optP --cpp

executables:
  boo:
    main:                Main.hs
    source-dirs:         app
    ghc-options:
    - -threaded
    - -rtsopts
    - -with-rtsopts=-N

As before, GHC 8.10.7 fails and GHC 9.2.7 works. In each case, the GHC command seems to be the same. Turning on GHC's verbosity too (eg stack --verbose --cabal-verbose --resolver lts-20.19 build --ghc-options "-v -keep-tmp-files"):

GHC 8.10.7

GHC's output (extract):

2023-05-06 14:16:39.007733: [warn] *** systool:cpp:
2023-05-06 14:16:39.007733: [warn] *** C pre-processor:
2023-05-06 14:16:39.007733: [warn] "cpphs"
"-include" ".stack-work\\dist\\274b403a\\build\\boo\\autogen\\cabal_macros.h" 
"--cpp" 
"-I.stack-work\\dist\\274b403a\\build\\boo\\boo-tmp" 
"-I.stack-work\\dist\\274b403a\\build\\boo\\boo-tmp" 
"-I.stack-work\\dist\\274b403a\\build\\boo\\autogen" 
"-I.stack-work\\dist\\274b403a\\build\\global-autogen" 
"-I.stack-work\\dist\\274b403a\\build\\boo\\boo-tmp" 
"-IC:\\Users\\mikep\\AppData\\Local\\Programs\\stack\\x86_64-windows\\msys2-20210604\\mingw64\\include" 
"-IC:\Users\mikep\AppData\Local\Programs\stack\x86_64-windows\ghc-8.10.7\lib\base-4.14.3.0\include" 
"-IC:\Users\mikep\AppData\Local\Programs\stack\x86_64-windows\ghc-8.10.7\lib\integer-gmp-1.0.3.0\include" 
"-IC:\Users\mikep\AppData\Local\Programs\stack\x86_64-windows\ghc-8.10.7\lib/include" 
"-include" "C:\Users\mikep\AppData\Local\Programs\stack\x86_64-windows\ghc-8.10.7\lib/include\ghcversion.h" 
"-Dmingw32_BUILD_OS" 
"-Dx86_64_BUILD_ARCH" 
"-Dmingw32_HOST_OS" 
"-Dx86_64_HOST_ARCH" 
"-D__GLASGOW_HASKELL_TH__" 
"-D__SSE__" 
"-D__SSE2__" 
"-includeC:\Users\mikep\AppData\Local\Temp\ghc12348_0\ghc_2.h" 
"-x" "assembler-with-cpp" 
"app\Main.hs" 
"-o" "C:\Users\mikep\AppData\Local\Temp\ghc12348_0\ghc_1.hscpp"

Output ghc_1.hscpp (extract)

#line 1 "app/Main.hs"
#line 1 "./.stack-work

GHC 9.2.7

GHC's output (extract):

2023-05-06 14:30:49.538259: [warn] *** systool:cpp:
2023-05-06 14:30:49.538259: [warn] *** C pre-processor:
2023-05-06 14:30:49.538259: [warn] "cpphs" 
"-include" ".stack-work\dist\8a54c84f\build\boo\autogen\cabal_macros.h" 
"--cpp" 
"-I.stack-work\dist\8a54c84f\build\boo\boo-tmp" 
"-I.stack-work\dist\8a54c84f\build\boo\boo-tmp" 
"-I.stack-work\dist\8a54c84f\build\boo\autogen" 
"-I.stack-work\dist\8a54c84f\build\global-autogen" 
"-I.stack-work\dist\8a54c84f\build\boo\boo-tmp" 
"-IC:\Users\mikep\AppData\Local\Programs\stack\x86_64-windows\msys2-20210604\mingw64\include" 
"-IC:\Users\mikep\AppData\Local\Programs\stack\x86_64-windows\ghc-9.2.7\lib\x86_64-windows-ghc-9.2.7\base-4.16.4.0\include" 
"-IC:\Users\mikep\AppData\Local\Programs\stack\x86_64-windows\ghc-9.2.7\lib\x86_64-windows-ghc-9.2.7\ghc-bignum-1.2\include" 
"-IC:\Users\mikep\AppData\Local\Programs\stack\x86_64-windows\ghc-9.2.7\lib\x86_64-windows-ghc-9.2.7\rts-1.0.2\include" 
"-include" "C:\Users\mikep\AppData\Local\Programs\stack\x86_64-windows\ghc-9.2.7\lib\x86_64-windows-ghc-9.2.7\rts-1.0.2\include\ghcversion.h" 
"-Dmingw32_BUILD_OS" 
"-Dx86_64_BUILD_ARCH" 
"-Dmingw32_HOST_OS" 
"-Dx86_64_HOST_ARCH" 
"-D__GLASGOW_HASKELL_TH__" 
"-D__SSE__" 
"-D__SSE2__" 
"-D__IO_MANAGER_WINIO__=1" 
"-D__IO_MANAGER_MIO__=1" 
"-includeC:\Users\mikep\AppData\Local\Temp\ghc23876_0\ghc_2.h" 
"-x" "assembler-with-cpp" 
"app\Main.hs" 
"-o" "C:\Users\mikep\AppData\Local\Temp\ghc23876_0\ghc_1.hscpp"

Output ghc_1.hscpp (extract):

#line 1 "app/Main.hs"
#line 1 "./.stack-work/dist/8a54c84f/build/boo/autogen/cabal_macros.h"

I think the key difference between GHC 8.7.10 and GHC 9.2.7 are these two corresponding lines in GHC's output:

"-include" ".stack-work\\dist\\274b403a\\build\\boo\\autogen\\cabal_macros.h" 
"-include" ".stack-work\dist\8a54c84f\build\boo\autogen\cabal_macros.h"

the first (GHC 8.7.10) has the \\ path separators that seem to be problemartic for cpphs (based on https://github.com/malcolmwallace/cpphs/issues/4). The second (GHC 9.2.7) does not have those path separators (it uses \).

So, my current hypothesis is that this is a change in GHC behaviour between GHC 8.10.7 and GHC 9.2.7, and the GHC 8.10.7 behaviour triggers a bug in cpphs.