Skip to content
New issue

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

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

Already on GitHub? Sign in to your account

Missing IsString instance with debug flags enabled #7081

Closed
kleinreact opened this issue Feb 2, 2024 · 5 comments · Fixed by #7092
Closed

Missing IsString instance with debug flags enabled #7081

kleinreact opened this issue Feb 2, 2024 · 5 comments · Fixed by #7092
Assignees
Labels
build Concerning building of Agda debug Concerning debug printing (not in changelog)
Milestone

Comments

@kleinreact
Copy link

Compiling Agda 2.6.4.1 on GHC 9.4.5 with the cabal flags debug, debug-parsing, and debug-serialisation enabled leads to the following erros:

src/full/Agda/Main.hs:291:5: error:
    • No instance for (Data.String.IsString (t0 -> [a0] -> [[Char]]))
        arising from the literal ‘"debug-parsing: enable printing grammars for operator parsing via '-v scope.grammar:10'"’
        (maybe you haven't applied a function to enough arguments?)
    • In the second argument of ‘(:)’, namely
        ‘"debug-parsing: enable printing grammars for operator parsing via '-v scope.grammar:10'"
           "debug-serialisation: extra debug info during serialisation into '.agdai' files"
           []’
      In the expression:
        "debug: enable debug printing ('-v' verbosity flags)"
          : "debug-parsing: enable printing grammars for operator parsing via '-v scope.grammar:10'"
              "debug-serialisation: extra debug info during serialisation into '.agdai' files"
              []
      In an equation for ‘flags’:
          flags
            = "debug: enable debug printing ('-v' verbosity flags)"
                : "debug-parsing: enable printing grammars for operator parsing via '-v scope.grammar:10'"
                    "debug-serialisation: extra debug info during serialisation into '.agdai' files"
                    []
    |
291 |     "debug-parsing: enable printing grammars for operator parsing via '-v scope.grammar:10'"
    |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

src/full/Agda/Main.hs:294:5: error:
    • Ambiguous type variable ‘t0’ arising from the literal ‘"debug-serialisation: extra debug info during serialisation into '.agdai' files"’
      prevents the constraint ‘(Data.String.IsString
                                  t0)’ from being solved.
      Probable fix: use a type annotation to specify what ‘t0’ should be.
      Potentially matching instances:
        instance (Data.String.IsString a, MonadIO m) =>
                 Data.String.IsString (TCMT m a)
          -- Defined at src/full/Agda/TypeChecking/Monad/Base.hs:5350:10
        instance (a ~ Char) => Data.String.IsString [a]
          -- Defined in ‘Data.String’
        ...plus 33 instances involving out-of-scope types
        (use -fprint-potential-instances to see them all)
    • In the first argument of ‘"debug-parsing: enable printing grammars for operator parsing via '-v scope.grammar:10'"’, namely
        ‘"debug-serialisation: extra debug info during serialisation into '.agdai' files"’
      In the second argument of ‘(:)’, namely
        ‘"debug-parsing: enable printing grammars for operator parsing via '-v scope.grammar:10'"
           "debug-serialisation: extra debug info during serialisation into '.agdai' files"
           []’
      In the expression:
        "debug: enable debug printing ('-v' verbosity flags)"
          : "debug-parsing: enable printing grammars for operator parsing via '-v scope.grammar:10'"
              "debug-serialisation: extra debug info during serialisation into '.agdai' files"
              []
    |
294 |     "debug-serialisation: extra debug info during serialisation into '.agdai' files"
    |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
@andreasabel
Copy link
Member

@UlfNorell : This issue points at gaps in our build matrix. Could you please add a configuration that would have exposed this issue?

include:
## Latest GHC, special builds
# Linux, without tests but with doctest
- os: ubuntu-22.04
description: Linux doctest
ghc-ver: '9.8.1'
# Can't leave cabal-flags empty here lest it becomes the default value.
cabal-flags: '--disable-tests'
doctest: true
# Linux, without -f enable-cluster-counting but with -f debug
- os: ubuntu-22.04
description: Linux debug
ghc-ver: '9.8.1'
cabal-flags: '--enable-tests -f debug'
# Linux, with containers-0.7 and everything
- os: ubuntu-22.04
description: Linux containers 0.7
ghc-ver: '9.8.1'
## Andreas, 2023-09-28: Test containers-0.7 here which has breaking changes.
## Note: -c 'containers >= 0.7' with single quotes does not get communicated properly.
## (The single quotes stay, and "-c 'containers" is an option parse error for cabal.)
cabal-flags: |
--enable-tests -f enable-cluster-counting -f debug -c containers>=0.7 --allow-newer=containers

@andreasabel andreasabel reopened this Feb 2, 2024
@andreasabel andreasabel added debug Concerning debug printing (not in changelog) infra: github workflows Issues related to GitHub workflows and actions (not in changelog) labels Feb 2, 2024
@andreasabel andreasabel added this to the 2.6.4.2 milestone Feb 2, 2024
@UlfNorell
Copy link
Member

I'll leave that to someone more familiar with the CI system. The test to add is compiling with all the debug flags turned on (-fdebug -fdebug-parsing -fdebug-serialisation).

@andreasabel
Copy link
Member

I'll leave that to someone more familiar with the CI system.

Could be your entry point into CI...

I just realized that the released 2.6.4.1 has this build problem while working on relaxing its ansi-terminal constraint.
I guess this calls for a patch release 2.6.4.2.

@UlfNorell
Copy link
Member

I wouldn't worry too much about this particular issue. -fdebug-parsing and -fdebug-serialisation are extremely niche flags that you only turn on if you are working on the operator parser or serialiser, and in that case you can fix any problems as you find them. I would argue it's not worth spending CI time or effort pushing out a hotfix release for this.

@andreasabel andreasabel modified the milestones: 2.6.5, 2.6.4.2 Feb 7, 2024
@andreasabel andreasabel self-assigned this Feb 7, 2024
@andreasabel
Copy link
Member

I don't want the latest release to have broken build paths.

@andreasabel andreasabel added build Concerning building of Agda and removed infra: github workflows Issues related to GitHub workflows and actions (not in changelog) labels Feb 7, 2024
@andreasabel andreasabel mentioned this issue Feb 8, 2024
3 tasks
andreasabel pushed a commit that referenced this issue Feb 8, 2024
VitalyAnkh pushed a commit to VitalyAnkh/agda that referenced this issue Mar 5, 2024
VitalyAnkh pushed a commit to VitalyAnkh/agda that referenced this issue Mar 5, 2024
JobPetrovcic pushed a commit to JobPetrovcic/agda that referenced this issue Apr 12, 2024
JobPetrovcic pushed a commit to JobPetrovcic/agda that referenced this issue Apr 12, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
build Concerning building of Agda debug Concerning debug printing (not in changelog)
Projects
None yet
Development

Successfully merging a pull request may close this issue.

3 participants