-
Notifications
You must be signed in to change notification settings - Fork 86
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
<details><summary>Timing</summary>
<p>
```
Time | Peak Mem | File Name
------------------------------------------------------------------------------------------------------
28m36.07s | 1742960 ko | Total Time / Peak Mem
------------------------------------------------------------------------------------------------------
3m30.41s | 1335360 ko | ToTemplate/QuotationOf/Common/Kernames/KernameMap/Instances.vo
3m21.62s | 1701848 ko | ToTemplate/QuotationOf/Coq/FSets/FMapAVL/Sig.vo
1m50.32s | 1606248 ko | ToTemplate/QuotationOf/Coq/MSets/MSetAVL/Sig.vo
1m25.21s | 1283592 ko | ToTemplate/QuotationOf/Common/Universes/ConstraintSet/Instances.vo
1m21.88s | 1284000 ko | ToTemplate/QuotationOf/Common/Kernames/KernameSet/Instances.vo
1m19.88s | 1742960 ko | ToTemplate/Coq/MSets.vo
1m15.76s | 1282544 ko | ToTemplate/QuotationOf/Common/Universes/LevelSet/Instances.vo
1m12.04s | 1368088 ko | ToTemplate/QuotationOf/Coq/MSets/MSetList/Sig.vo
0m58.84s | 1057848 ko | ToTemplate/QuotationOf/Common/Universes/ConstraintSetOrdProp/Instances.vo
0m56.64s | 1034060 ko | ToTemplate/QuotationOf/Common/Universes/LevelExprSetOrdProp/Instances.vo
0m56.61s | 1004488 ko | ToTemplate/QuotationOf/Common/Kernames/KernameSetOrdProp/Instances.vo
0m53.50s | 1016636 ko | ToTemplate/QuotationOf/Common/Universes/LevelSetOrdProp/Instances.vo
0m51.59s | 1138188 ko | ToTemplate/QuotationOf/Common/Universes/LevelExprSet/Instances.vo
0m49.75s | 1379420 ko | ToTemplate/Coq/FSets.vo
0m49.74s | 1107368 ko | ToTemplate/QuotationOf/Coq/MSets/MSetProperties/Sig.vo
0m42.10s | 1256528 ko | ToTemplate/QuotationOf/Common/EnvironmentTyping/Sig.vo
0m37.84s | 1016312 ko | ToTemplate/QuotationOf/Coq/FSets/FMapList/Sig.vo
0m34.52s | 1013440 ko | ToTemplate/QuotationOf/Common/Environment/Sig.vo
0m22.88s | 852064 ko | ToTemplate/QuotationOf/Template/Ast/Env/Instances.vo
0m21.17s | 877048 ko | ToTemplate/QuotationOf/Coq/Structures/OrdersFacts/Sig.vo
0m19.04s | 1263092 ko | ToTemplate/Common/EnvironmentTyping.vo
0m18.07s | 841212 ko | ToTemplate/QuotationOf/Coq/MSets/MSetDecide/Sig.vo
0m17.21s | 834976 ko | ToTemplate/QuotationOf/Coq/Structures/OrdersAlt/Sig.vo
0m15.02s | 1075516 ko | ToTemplate/Template/Typing.vo
0m14.61s | 905324 ko | ToTemplate/Common/Universes.vo
0m13.40s | 816856 ko | ToTemplate/QuotationOf/Template/Typing/TemplateGlobalMaps/Instances.vo
0m13.34s | 780536 ko | ToTemplate/QuotationOf/Coq/MSets/MSetFacts/Sig.vo
0m12.93s | 774728 ko | ToTemplate/QuotationOf/Coq/FSets/FMapFacts/Sig.vo
0m11.78s | 862636 ko | ToTemplate/Common/Kernames.vo
0m10.00s | 828792 ko | ToTemplate/QuotationOf/Template/Typing/TemplateEnvTyping/Instances.vo
0m08.93s | 725948 ko | ToTemplate/QuotationOf/Common/Kernames/KernameMapFact/Instances.vo
0m07.23s | 728332 ko | ToTemplate/QuotationOf/Coq/MSets/MSetInterface/Sig.vo
0m06.99s | 705852 ko | ToTemplate/QuotationOf/Coq/Structures/Equalities/Sig.vo
0m05.96s | 725548 ko | ToTemplate/QuotationOf/Coq/FSets/FMapInterface/Sig.vo
0m05.11s | 992248 ko | ToTemplate/Template/TermEquality.vo
0m04.96s | 761740 ko | ToTemplate/QuotationOf/Template/Ast/TemplateLookup/Instances.vo
0m04.71s | 932436 ko | ToTemplate/Common/Environment.vo
0m04.53s | 989628 ko | ToTemplate/Template/WfAst.vo
0m03.78s | 769156 ko | ToTemplate/QuotationOf/Template/Typing/TemplateConversion/Instances.vo
0m03.18s | 713016 ko | ToTemplate/QuotationOf/Coq/Structures/OrdersTac/Sig.vo
0m02.95s | 701344 ko | ToTemplate/QuotationOf/Common/Universes/Level/Instances.vo
0m02.90s | 756624 ko | ToTemplate/QuotationOf/Template/Typing/TemplateDeclarationTyping/Instances.vo
0m02.86s | 703056 ko | ToTemplate/QuotationOf/Coq/Structures/Orders/Sig.vo
0m02.64s | 698816 ko | ToTemplate/QuotationOf/Common/Kernames/Kername/Instances.vo
0m02.53s | 922916 ko | ToTemplate/QuotationOf/Template/Ast/EnvHelper/Instances.vo
0m02.49s | 699500 ko | ToTemplate/QuotationOf/Common/Universes/LevelExpr/Instances.vo
0m02.12s | 984776 ko | ToTemplate/Template/Ast.vo
0m02.01s | 700412 ko | ToTemplate/Coq/Init.vo
0m01.99s | 701512 ko | ToTemplate/QuotationOf/Common/Universes/UnivConstraint/Instances.vo
0m01.98s | 704288 ko | ToTemplate/Utils/utils.vo
0m01.87s | 709068 ko | ToTemplate/QuotationOf/Template/Ast/TemplateTerm/Instances.vo
0m01.82s | 696724 ko | ToTemplate/Utils/MCUtils.vo
0m01.63s | 713200 ko | ToTemplate/QuotationOf/Template/ReflectAst/EnvDecide/Instances.vo
0m01.62s | 695876 ko | ToTemplate/Init.vo
0m01.53s | 696780 ko | ToTemplate/Coq/Lists.vo
0m01.49s | 699684 ko | ToTemplate/Utils/All_Forall.vo
0m01.43s | 695080 ko | ToTemplate/Utils/MCProd.vo
0m01.34s | 696508 ko | ToTemplate/Utils/ReflectEq.vo
0m01.27s | 697288 ko | ToTemplate/Utils/MCOption.vo
0m01.26s | 980920 ko | ToTemplate/Template/AstUtils.vo
0m01.23s | 693944 ko | ToTemplate/Coq/Bool.vo
0m01.22s | 755464 ko | ToTemplate/QuotationOf/Template/Typing/TemplateConversionPar/Instances.vo
0m01.20s | 757612 ko | ToTemplate/QuotationOf/Template/Typing/TemplateTyping/Instances.vo
0m01.19s | 710540 ko | ToTemplate/QuotationOf/Template/ReflectAst/TemplateTermDecide/Instances.vo
0m01.18s | 694060 ko | ToTemplate/Utils/MCList.vo
0m01.15s | 697976 ko | CommonUtils.vo
0m01.12s | 955240 ko | ToTemplate/QuotationOf/Template/Ast/Instances.vo
0m01.12s | 706104 ko | ToTemplate/QuotationOf/Template/Ast/TemplateTermUtils/Instances.vo
0m01.08s | 867856 ko | ToTemplate/Common/BasicAst.vo
0m01.07s | 695148 ko | ToTemplate/Utils/bytestring.vo
0m01.06s | 693992 ko | ToTemplate/Utils/MCArith.vo
0m01.03s | 703564 ko | ToTemplate/Coq/Floats.vo
0m00.98s | 700584 ko | ToTemplate/Coq/Numbers.vo
0m00.98s | 694564 ko | ToTemplate/Utils/MCReflect.vo
0m00.88s | 756228 ko | ToTemplate/QuotationOf/Template/Typing/Instances.vo
0m00.87s | 695256 ko | ToTemplate/Coq/Strings.vo
0m00.86s | 766292 ko | ToTemplate/QuotationOf/Common/Kernames/Instances.vo
0m00.84s | 696340 ko | ToTemplate/Coq/ssr.vo
0m00.83s | 694736 ko | ToTemplate/Common/Primitive.vo
0m00.83s | 698224 ko | ToTemplate/Common/config.vo
0m00.81s | 745564 ko | ToTemplate/QuotationOf/Common/Universes/Instances.vo
0m00.80s | 700668 ko | ToTemplate/QuotationOf/Template/ReflectAst/Instances.vo
0m00.20s | 63332 ko | ToTemplate/Utils/monad_utils.vo
0m00.08s | 64744 ko | ToTemplate/Utils/MCRelations.vo
0m00.06s | 64376 ko | ToTemplate/Utils/MCString.vo
0m00.05s | 64560 ko | ToTemplate/Common/Reflect.vo
0m00.05s | 63284 ko | ToTemplate/Template/ReflectAst.vo
0m00.05s | 65008 ko | ToTemplate/Utils/MCPrelude.vo
0m00.05s | 65068 ko | ToTemplate/Utils/MCSquash.vo
0m00.04s | 64248 ko | ToTemplate/Template/Induction.vo
0m00.04s | 64996 ko | ToTemplate/Template/LiftSubst.vo
0m00.04s | 64736 ko | ToTemplate/Template/UnivSubst.vo
0m00.04s | 64308 ko | ToTemplate/Utils/MCCompare.vo
0m00.04s | 63324 ko | ToTemplate/Utils/MCEquality.vo
0m00.04s | 65020 ko | ToTemplate/Utils/wGraph.vo
0m00.03s | 64724 ko | ToTemplate/Utils/ByteCompare.vo
0m00.03s | 63432 ko | ToTemplate/Utils/ByteCompareSpec.vo
0m00.03s | 64856 ko | ToTemplate/Utils/LibHypsNaming.vo
0m00.03s | 64768 ko | ToTemplate/Utils/MCPred.vo
0m00.02s | 65064 ko | ToTemplate/Common/Transform.vo
0m00.01s | 64484 ko | ToTemplate/Utils/ByteCompare_opt.vo
```
</p>
</details>- Loading branch information
1 parent
708c53b
commit 38381e8
Showing
124 changed files
with
4,598 additions
and
15 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,37 @@ | ||
| opam-version: "2.0" | ||
| version: "8.16.dev" | ||
| maintainer: "matthieu.sozeau@inria.fr" | ||
| homepage: "https://metacoq.github.io/metacoq" | ||
| dev-repo: "git+https://github.com/MetaCoq/metacoq.git#coq-8.16" | ||
| bug-reports: "https://github.com/MetaCoq/metacoq/issues" | ||
| authors: ["Abhishek Anand <aa755@cs.cornell.edu>" | ||
| "Danil Annenkov <danil.v.annenkov@gmail.com>" | ||
| "Simon Boulier <simon.boulier@inria.fr>" | ||
| "Cyril Cohen <cyril.cohen@inria.fr>" | ||
| "Yannick Forster <forster@ps.uni-saarland.de>" | ||
| "Jason Gross <jgross@mit.edu>" | ||
| "Fabian Kunze <fkunze@fakusb.de>" | ||
| "Meven Lennon-Bertrand <Meven.Bertrand@univ-nantes.fr>" | ||
| "Kenji Maillard <kenji.maillard@inria.fr>" | ||
| "Gregory Malecha <gmalecha@gmail.com>" | ||
| "Jakob Botsch Nielsen <Jakob.botsch.nielsen@gmail.com>" | ||
| "Matthieu Sozeau <matthieu.sozeau@inria.fr>" | ||
| "Nicolas Tabareau <nicolas.tabareau@inria.fr>" | ||
| "Théo Winterhalter <theo.winterhalter@inria.fr>" | ||
| ] | ||
| license: "MIT" | ||
| build: [ | ||
| ["bash" "./configure.sh"] | ||
| [make "-j" "%{jobs}%" "-C" "quotation"] | ||
| ] | ||
| install: [ | ||
| [make "-C" "quotation" "install"] | ||
| ] | ||
| depends: [ | ||
| "coq-metacoq-template" {= version} | ||
| "coq-metacoq-pcuic" {= version} | ||
| "coq-metacoq-template-pcuic" {= version} | ||
| ] | ||
| synopsis: "Gallina quotation functions for Template Coq and PCUIC." | ||
| description: """ | ||
| """ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,33 @@ | ||
| all: theory | ||
|
|
||
| _CoqProject: _CoqProject.in metacoq-config | ||
| cat metacoq-config > _CoqProject | ||
| cat _CoqProject.in >> _CoqProject | ||
|
|
||
| Makefile.quotation: _CoqProject | ||
| coq_makefile -f _CoqProject -o Makefile.quotation $(DEPS) | ||
|
|
||
| theory: Makefile.quotation | ||
| $(MAKE) -f Makefile.quotation | ||
|
|
||
| install: theory | ||
| $(MAKE) -f Makefile.quotation install | ||
|
|
||
| uninstall: Makefile.quotation | ||
| $(MAKE) -f Makefile.quotation uninstall | ||
|
|
||
| clean: Makefile.quotation | ||
| make -f Makefile.quotation clean | ||
|
|
||
| mrproper: | ||
| rm -f metacoq-config | ||
| rm -f Makefile.quotation _CoqProject | ||
|
|
||
| .merlin: | ||
| make -f $< $@ | ||
|
|
||
| vos: Makefile.quotation | ||
| $(MAKE) -f Makefile.quotation vos | ||
|
|
||
| quick: Makefile.quotation | ||
| $(MAKE) -f Makefile.quotation COQEXTRAFLAGS="-unset \"Universe Checking\"" vos |
Oops, something went wrong.