Skip to content

[Draft] Deeper integration with Agda: foundational work #97

[Draft] Deeper integration with Agda: foundational work

[Draft] Deeper integration with Agda: foundational work #97

Re-run triggered November 5, 2025 17:51
Status Failure
Total duration 1h 47m 16s
Artifacts 8

test.yaml

on: pull_request
Matrix: Build and Test
Build WASM
0s
Build WASM
Create Release
0s
Create Release
Upload to Stable Release
0s
Upload to Stable Release
Upload to Dev Release
0s
Upload to Dev Release
Fit to window
Zoom out
Zoom in

Annotations

20 errors and 3 notices
Build and Test (ubuntu-latest, Agda-2.6.4.3)
Process completed with exit code 1.
Build and Test (macos-latest, Agda-2.6.4.3)
Process completed with exit code 1.
Build and Test (macos-latest, Agda-2.6.4.3): src/Server/Model/Handler.hs#L90
• Could not deduce ‘TCM.PrettyTCM TCM.TCErr’
Build and Test (macos-latest, Agda-2.6.4.3): src/Server/Model/Handler.hs#L53
• Could not deduce ‘TCM.PrettyTCM TCM.TCErr’
Build and Test (macos-latest, Agda-2.6.4.3): src/Indexer/Indexer.hs#L565
Not in scope: data constructor ‘A.OverlapPragma’
Build and Test (macos-latest, Agda-2.6.4.3): src/Indexer/Indexer.hs#L559
Not in scope: data constructor ‘A.InjectiveForInferencePragma’
Build and Test (macos-latest, Agda-2.6.4.3): src/Indexer/Indexer.hs#L394
Not in scope: data constructor ‘C.LeftLet’
Build and Test (macos-latest, Agda-2.6.4.3): src/Indexer/Indexer.hs#L305
Not in scope: type constructor or class ‘A.TacticAttribute’
Build and Test (macos-latest, Agda-2.6.4.3): src/Agda/Syntax/Abstract/More.hs#L10
Module ‘Agda.Syntax.Concrete’ does not export ‘TacticAttribute'’.
Build and Test (macos-latest, Agda-2.6.4.3): src/Agda/Interaction/Imports/More.hs#L63
Module ‘Agda.TypeChecking.Monad’ does not export ‘checkAndSetOptionsFromPragma’.
Build and Test (windows-latest, Agda-2.6.4.3)
Process completed with exit code 1.
Build and Test (macos-13, Agda-2.6.4.3)
Process completed with exit code 1.
Build and Test (macos-13, Agda-2.6.4.3): src/Server/Model/Handler.hs#L90
• Could not deduce ‘TCM.PrettyTCM TCM.TCErr’
Build and Test (macos-13, Agda-2.6.4.3): src/Server/Model/Handler.hs#L53
• Could not deduce ‘TCM.PrettyTCM TCM.TCErr’
Build and Test (macos-13, Agda-2.6.4.3): src/Indexer/Indexer.hs#L565
Not in scope: data constructor ‘A.OverlapPragma’
Build and Test (macos-13, Agda-2.6.4.3): src/Indexer/Indexer.hs#L559
Not in scope: data constructor ‘A.InjectiveForInferencePragma’
Build and Test (macos-13, Agda-2.6.4.3): src/Indexer/Indexer.hs#L394
Not in scope: data constructor ‘C.LeftLet’
Build and Test (macos-13, Agda-2.6.4.3): src/Indexer/Indexer.hs#L305
Not in scope: type constructor or class ‘A.TacticAttribute’
Build and Test (macos-13, Agda-2.6.4.3): src/Agda/Syntax/Abstract/More.hs#L10
Module ‘Agda.Syntax.Concrete’ does not export ‘TacticAttribute'’.
Build and Test (macos-13, Agda-2.6.4.3): src/Agda/Interaction/Imports/More.hs#L63
Module ‘Agda.TypeChecking.Monad’ does not export ‘checkAndSetOptionsFromPragma’.
Build and Test (macos-13, Agda-2.7.0.1)
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
Build and Test (macos-13, Agda-2.8.0)
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
Build and Test (macos-13, Agda-2.6.4.3)
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

Artifacts

Produced during runtime
Name Size Digest
als-Agda-2.7.0.1-macos-arm64 Expired
44.4 MB
sha256:212ab2882abbce584b4473ba31a525b08f9b8cf5d4b45cff591a89577e9bd5c7
als-Agda-2.7.0.1-macos-x64 Expired
24.2 MB
sha256:1aea55b641fad0e134c4058e8b8bbd72ae63c89676de25e52639e024cdeff064
als-Agda-2.7.0.1-ubuntu Expired
18.2 MB
sha256:9efe45094030a1f1a466bf50e4de362ea22004ce4d5dbe64f7570153b5e3f571
als-Agda-2.7.0.1-windows Expired
35.8 MB
sha256:6e040be8869041b9b3d952f8ce700bdc4b726b265227f825b9b8bab312b2e47d
als-Agda-2.8.0-macos-arm64 Expired
49.6 MB
sha256:6528fa579be4d78eec3fe6fbc50ba598dffd1418883375a6f23da86478397040
als-Agda-2.8.0-macos-x64 Expired
27.5 MB
sha256:e447a249bcdb5be961a15242d54053b23ce9354fc0291f282fde3176ed15bbcc
als-Agda-2.8.0-ubuntu Expired
21.2 MB
sha256:6fa07255eca32806240c6bcf4690ccaea6ddbed68eabfd13591569a4fcd4400a
als-Agda-2.8.0-windows Expired
38.9 MB
sha256:3337230ef64cf18560b6d8ea6561ee85adda93c7edebdf9eabd45a947cf21317