[Draft] Deeper integration with Agda: foundational work #97
Annotations
9 errors and 1 notice
|
🏗️ Build ALS
Process completed with exit code 1.
|
|
🏗️ Build ALS:
src/Server/Model/Handler.hs#L90
• Could not deduce ‘TCM.PrettyTCM TCM.TCErr’
|
|
🏗️ Build ALS:
src/Server/Model/Handler.hs#L53
• Could not deduce ‘TCM.PrettyTCM TCM.TCErr’
|
|
🏗️ Build ALS:
src/Indexer/Indexer.hs#L565
Not in scope: data constructor ‘A.OverlapPragma’
|
|
🏗️ Build ALS:
src/Indexer/Indexer.hs#L559
Not in scope: data constructor ‘A.InjectiveForInferencePragma’
|
|
🏗️ Build ALS:
src/Indexer/Indexer.hs#L394
Not in scope: data constructor ‘C.LeftLet’
|
|
🏗️ Build ALS:
src/Indexer/Indexer.hs#L305
Not in scope: type constructor or class ‘A.TacticAttribute’
|
|
🏗️ Build ALS:
src/Agda/Syntax/Abstract/More.hs#L10
Module ‘Agda.Syntax.Concrete’ does not export ‘TacticAttribute'’.
|
|
🏗️ Build ALS:
src/Agda/Interaction/Imports/More.hs#L63
Module ‘Agda.TypeChecking.Monad’ does not export ‘checkAndSetOptionsFromPragma’.
|
|
The macOS-13 based runner images are being deprecated, consider switching to macOS-15 (macos-15-intel) or macOS 15 arm64 (macos-latest) instead. For more details see https://github.com/actions/runner-images/issues/13046
|
Loading