Skip to content
New issue

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

#

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

Already on GitHub? # to your account

Jump to bottom

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

Closed
andreasabel opened this issue Apr 27, 2023 · 19 comments
Closed

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

andreasabel opened this issue Apr 27, 2023 · 19 comments
Labels
resolution: upstream issue

Comments

@andreasabel
Copy link

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?
@andreasabel andreasabel mentioned this issue Apr 27, 2023
Merged
5 tasks
@hasufell
Copy link
Contributor

Have you tried with choco installed 9.4.5?

@andreasabel
Copy link
Author

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
Copy link
Author

andreasabel commented Apr 28, 2023 •
edited
Loading

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:

This was referenced Apr 28, 2023
Merged
Closed
@andreasabel
Copy link
Author

andreasabel commented Apr 28, 2023 •
edited
Loading

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

  • stack-2.9.3
  • ghc-9.4.5 or 9.4.4 (via ghcup)
  • stackage nightly (both for 9.4.4 (2023-04-24) and 9.4.5 (2023-04-25))

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 andreasabel mentioned this issue Apr 28, 2023
Closed
@andreasabel
Copy link
Author

andreasabel commented Apr 28, 2023 •
edited
Loading

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
Copy link
Contributor

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

@andreasabel
Copy link
Author

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

Good question, let me try to find out.

@andreasabel
Copy link
Author

andreasabel commented Apr 28, 2023 •
edited
Loading

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
Copy link
Contributor

agda/agda#1285

Hmm

@andreasabel
Copy link
Author

andreasabel commented Apr 28, 2023 •
edited
Loading

@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
Copy link
Member

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
Copy link
Contributor

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
Copy link
Member

mpilgrem commented Apr 29, 2023 •
edited
Loading

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

This was referenced Apr 30, 2023
Closed
Draft
@andreasabel
Copy link
Author

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
Copy link
Member

mpilgrem commented May 5, 2023

@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.

@mpilgrem mpilgrem closed this as completed May 5, 2023
@andreasabel
Copy link
Author

@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
Copy link
Member

mpilgrem commented May 6, 2023 •
edited
Loading

@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: malcolmwallace/cpphs#4

@andreasabel
Copy link
Author

@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
Copy link
Member

mpilgrem commented May 6, 2023

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 malcolmwallace/cpphs#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.

# for free to join this conversation on GitHub. Already have an account? # to comment
Assignees
No one assigned
Labels
resolution: upstream issue
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@andreasabel @hasufell @mpilgrem