[Draft] Reintegrate Framework V2 into Framework V1 #39
Annotations
10 errors, 1 warning, and 1 notice
|
Check Agda files:
src/Translation/Lang/VariantList-to-CCC.lagda.md#L20
The name of the top level module does not match the file name. The
module Translation.VariantList-to-CCC should be defined in one of
the following files:
/nix/store/w2pzcxa92a1vi5g62as8h8hcyav9sfp2-standard-library-1.7.2/src/Translation/VariantList-to-CCC.agda
/nix/store/w2pzcxa92a1vi5g62as8h8hcyav9sfp2-standard-library-1.7.2/src/Translation/VariantList-to-CCC.lagda
/home/runner/work/AgdaCCnOC/AgdaCCnOC/src/Translation/VariantList-to-CCC.agda
/home/runner/work/AgdaCCnOC/AgdaCCnOC/src/Translation/VariantList-to-CCC.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/VariantList-to-CCC.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/VariantList-to-CCC.lagda
|
|
Check Agda files:
src/Translation/Lang/2ADT-to-NADT.agda#L4
The name of the top level module does not match the file name. The
module Framework.V2.Translation.Lang.2ADT-to-NADT should be defined
in one of the following files:
/home/runner/work/AgdaCCnOC/Framework/V2/Translation/Lang/2ADT-to-NADT.agda
/home/runner/work/AgdaCCnOC/Framework/V2/Translation/Lang/2ADT-to-NADT.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/Translation/Lang/2ADT-to-NADT.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/Translation/Lang/2ADT-to-NADT.lagda
|
|
Check Agda files:
src/Translation/Lang/OC-to-BCC.lagda.md#L16
The name of the top level module does not match the file name. The
module Translation.OC-to-BCC should be defined in one of the
following files:
/nix/store/w2pzcxa92a1vi5g62as8h8hcyav9sfp2-standard-library-1.7.2/src/Translation/OC-to-BCC.agda
/nix/store/w2pzcxa92a1vi5g62as8h8hcyav9sfp2-standard-library-1.7.2/src/Translation/OC-to-BCC.lagda
/home/runner/work/AgdaCCnOC/AgdaCCnOC/src/Translation/OC-to-BCC.agda
/home/runner/work/AgdaCCnOC/AgdaCCnOC/src/Translation/OC-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/OC-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/OC-to-BCC.lagda
|
|
Check Agda files:
src/Translation/Construct/NChoice-to-2Choice.agda#L2
The name of the top level module does not match the file name. The
module Framework.V2.Translation.Construct.NChoice-to-2Choice should
be defined in one of the following files:
/home/runner/work/AgdaCCnOC/Framework/V2/Translation/Construct/NChoice-to-2Choice.agda
/home/runner/work/AgdaCCnOC/Framework/V2/Translation/Construct/NChoice-to-2Choice.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/Translation/Construct/NChoice-to-2Choice.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/Translation/Construct/NChoice-to-2Choice.lagda
|
|
Check Agda files:
src/Translation/Construct/2Choice-to-NChoice.agda#L2
The name of the top level module does not match the file name. The
module Framework.V2.Translation.Construct.2Choice-to-NChoice should
be defined in one of the following files:
/home/runner/work/AgdaCCnOC/Framework/V2/Translation/Construct/2Choice-to-NChoice.agda
/home/runner/work/AgdaCCnOC/Framework/V2/Translation/Construct/2Choice-to-NChoice.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/Translation/Construct/2Choice-to-NChoice.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/Translation/Construct/2Choice-to-NChoice.lagda
|
|
Check Agda files:
src/Translation/Construct/NestedChoice-to-2Choice.agda#L3
The name of the top level module does not match the file name. The
module Framework.V2.Translation.Construct.NestedChoice-to-2Choice
should be defined in one of the following files:
/home/runner/work/AgdaCCnOC/Framework/V2/Translation/Construct/NestedChoice-to-2Choice.agda
/home/runner/work/AgdaCCnOC/Framework/V2/Translation/Construct/NestedChoice-to-2Choice.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/Translation/Construct/NestedChoice-to-2Choice.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/Translation/Construct/NestedChoice-to-2Choice.lagda
|
|
Check Agda files:
src/Translation/Construct/2Choice-to-NChoice-VL.agda#L3
The name of the top level module does not match the file name. The
module Framework.V2.Translation.Construct.2Choice-to-NChoice-VL
should be defined in one of the following files:
/home/runner/work/AgdaCCnOC/Framework/V2/Translation/Construct/2Choice-to-NChoice-VL.agda
/home/runner/work/AgdaCCnOC/Framework/V2/Translation/Construct/2Choice-to-NChoice-VL.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/Translation/Construct/2Choice-to-NChoice-VL.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/Translation/Construct/2Choice-to-NChoice-VL.lagda
|
|
Check Agda files:
src/Translation/LanguageMap.lagda.md#L33
Failed to find source of module Framework.Relation.Expressiveness
in any of the following locations:
/nix/store/w2pzcxa92a1vi5g62as8h8hcyav9sfp2-standard-library-1.7.2/src/Framework/Relation/Expressiveness.agda
/nix/store/w2pzcxa92a1vi5g62as8h8hcyav9sfp2-standard-library-1.7.2/src/Framework/Relation/Expressiveness.lagda
/home/runner/work/AgdaCCnOC/AgdaCCnOC/src/Framework/Relation/Expressiveness.agda
/home/runner/work/AgdaCCnOC/AgdaCCnOC/src/Framework/Relation/Expressiveness.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/Relation/Expressiveness.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/Relation/Expressiveness.lagda
when scope checking the declaration
open import Framework.Relation.Expressiveness
———— Warning(s) ————————————————————————————————————————————
|
|
Check Agda files:
src/Translation/Deprecated/BCC-to-CCC.lagda.md#L12
The name of the top level module does not match the file name. The
module Translation.BCC-to-CCC should be defined in one of the
following files:
/nix/store/w2pzcxa92a1vi5g62as8h8hcyav9sfp2-standard-library-1.7.2/src/Translation/BCC-to-CCC.agda
/nix/store/w2pzcxa92a1vi5g62as8h8hcyav9sfp2-standard-library-1.7.2/src/Translation/BCC-to-CCC.lagda
/home/runner/work/AgdaCCnOC/AgdaCCnOC/src/Translation/BCC-to-CCC.agda
/home/runner/work/AgdaCCnOC/AgdaCCnOC/src/Translation/BCC-to-CCC.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/BCC-to-CCC.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/BCC-to-CCC.lagda
|
|
Check Agda files:
src/Translation/Deprecated/CCC-to-BCC.lagda.md#L13
The name of the top level module does not match the file name. The
module Translation.CCC-to-BCC should be defined in one of the
following files:
/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
|
|
Node.js 16 actions are deprecated. Please update the following actions to use Node.js 20: actions/cache/restore@v3, actions/cache/save@v3. For more information see: https://github.blog/changelog/2023-09-22-github-actions-transitioning-from-node-16-to-node-20/.
|
|
Check Agda files
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)
|
The logs for this run have expired and are no longer available.
Loading