Skip to content
Check the Agda files

[Draft] Reintegrate Framework V2 into Framework V1 #34

Sign in to view logs

[Draft] Reintegrate Framework V2 into Framework V1

[Draft] Reintegrate Framework V2 into Framework V1 #34

Triggered via pull request December 6, 2023 19:06
@pmbittnerpmbittner
opened #14
wedding
Status Failure
Total duration 16m 40s
Artifacts –

check.yml

on: pull_request
build
16m 28s
build
Fit to window
Zoom out
Zoom in

Annotations

10 errors and 1 notice
build: src/Framework/TODO.lagda.md#L4
The name of the top level module does not match the file name. The module Framework.V2.TODO should be defined in one of the following files: /nix/store/w2pzcxa92a1vi5g62as8h8hcyav9sfp2-standard-library-1.7.2/src/Framework/V2/TODO.agda /nix/store/w2pzcxa92a1vi5g62as8h8hcyav9sfp2-standard-library-1.7.2/src/Framework/V2/TODO.lagda /home/runner/work/AgdaCCnOC/AgdaCCnOC/src/Framework/V2/TODO.agda /home/runner/work/AgdaCCnOC/AgdaCCnOC/src/Framework/V2/TODO.lagda /nix/store/s6774vfjza5r4dywxi8sgkdmq11nijsj-Agda-2.6.3-data/share/ghc-9.2.7/x86_64-linux-ghc-9.2.7/Agda-2.6.3/lib/prim/Framework/V2/TODO.agda /nix/store/s6774vfjza5r4dywxi8sgkdmq11nijsj-Agda-2.6.3-data/share/ghc-9.2.7/x86_64-linux-ghc-9.2.7/Agda-2.6.3/lib/prim/Framework/V2/TODO.lagda
build: src/Framework/Relation/Syntactic.lagda.md#L29
Not in scope: 𝕃 at /home/runner/work/AgdaCCnOC/AgdaCCnOC/src/Framework/Relation/Syntactic.lagda.md:29,16-17 when scope checking 𝕃
build: src/Test/Experiments/OC-to-BCC.agda#L25
Failed to find source of module Framework.Proof.Translation in any of the following locations: /nix/store/w2pzcxa92a1vi5g62as8h8hcyav9sfp2-standard-library-1.7.2/src/Framework/Proof/Translation.agda /nix/store/w2pzcxa92a1vi5g62as8h8hcyav9sfp2-standard-library-1.7.2/src/Framework/Proof/Translation.lagda /home/runner/work/AgdaCCnOC/AgdaCCnOC/src/Framework/Proof/Translation.agda /home/runner/work/AgdaCCnOC/AgdaCCnOC/src/Framework/Proof/Translation.lagda /nix/store/s6774vfjza5r4dywxi8sgkdmq11nijsj-Agda-2.6.3-data/share/ghc-9.2.7/x86_64-linux-ghc-9.2.7/Agda-2.6.3/lib/prim/Framework/Proof/Translation.agda /nix/store/s6774vfjza5r4dywxi8sgkdmq11nijsj-Agda-2.6.3-data/share/ghc-9.2.7/x86_64-linux-ghc-9.2.7/Agda-2.6.3/lib/prim/Framework/Proof/Translation.lagda when scope checking the declaration open import Framework.Proof.Translation using (expr) ———— Warning(s) ————————————————————————————————————————————
build: src/Test/Experiments/OC-to-BCC.agda#L21
The module Lang.OC doesn't export the following: ⟦_⟧ when scope checking the declaration open Lang.OC renaming (⟦_⟧ to ⟦_⟧-oc; Configuration to Conf-oc)
build: src/Test/Experiments/OC-to-BCC.agda#L22
The module Lang.BCC doesn't export the following: ⟦_⟧ when scope checking the declaration open Lang.BCC renaming (⟦_⟧ to ⟦_⟧-bcc; Configuration to Conf-bcc)
build: src/Test/Experiments/CCC-to-BCC.agda#L33
Failed to find source of module Translation.CCC-to-BCC in any of the following locations: /nix/store/w2pzcxa92a1vi5g62as8h8hcyav9sfp2-standard-library-1.7.2/src/Translation/CCC-to-BCC.agda /nix/store/w2pzcxa92a1vi5g62as8h8hcyav9sfp2-standard-library-1.7.2/src/Translation/CCC-to-BCC.lagda /home/runner/work/AgdaCCnOC/AgdaCCnOC/src/Translation/CCC-to-BCC.agda /home/runner/work/AgdaCCnOC/AgdaCCnOC/src/Translation/CCC-to-BCC.lagda /nix/store/s6774vfjza5r4dywxi8sgkdmq11nijsj-Agda-2.6.3-data/share/ghc-9.2.7/x86_64-linux-ghc-9.2.7/Agda-2.6.3/lib/prim/Translation/CCC-to-BCC.agda /nix/store/s6774vfjza5r4dywxi8sgkdmq11nijsj-Agda-2.6.3-data/share/ghc-9.2.7/x86_64-linux-ghc-9.2.7/Agda-2.6.3/lib/prim/Translation/CCC-to-BCC.lagda when scope checking the declaration open import Translation.CCC-to-BCC using (CCC→BCC) ———— Warning(s) ————————————————————————————————————————————
build: src/Test/Examples/Variants.agda#L11
Set !=< Agda.Builtin.Size.Size when checking that the expression Rose has type Framework.Definitions.𝕍
build: src/Test/Examples/OC.agda#L19
Not in scope: Artifact at /home/runner/work/AgdaCCnOC/AgdaCCnOC/src/Test/Examples/OC.agda:19,17-25 when scope checking Artifact ———— Warning(s) ————————————————————————————————————————————
build: src/Test/Examples/OC.agda#L9
The module Framework.Annotation.Name doesn't export the following: Option when scope checking the declaration open import Framework.Annotation.Name using (Option)
build: src/Test/Examples/CCC.agda#L25
Not in scope: leaves at /home/runner/work/AgdaCCnOC/AgdaCCnOC/src/Test/Examples/CCC.agda:25,24-30 (did you mean 'Agda.Primitive.Level'?) when scope checking leaves
build
The following files couldn't be checked because a dependency of them has errors: Test/Experiments/OC-to-BCC.agda (depends on ————) Test/Examples/OC.agda (depends on ————) Main.agda (depends on Test/Examples/CCC.agda) Test/Test/VariantList-Completeness.agda (depends on Test/Examples/Variants.agda) Test/Experiments/CCC-to-BCC.agda (depends on Test/Experiments/CCC-to-BCC.agda:29,3-30,25\nThe) Translation/LanguageMap.lagda.md (depends on Translation/LanguageMap.lagda.md:24,6-27,13\nThe)