From 3f0ee9508204e3ba2d1784d1f9d46c8306343860 Mon Sep 17 00:00:00 2001 From: mike dupont Date: Wed, 31 Jan 2024 05:29:02 -0500 Subject: [PATCH] coq reflection --- .gitmodules | 102 ++++++++++++++++++++++++ 2024/01/29/uttsolver | 1 + 2024/01/31/SepLogicTypeclasses | 1 + 2024/01/31/bedrock | 1 + 2024/01/31/coq-a-la-carte-cpp20 | 1 + 2024/01/31/coq-elpi | 1 + 2024/01/31/coq-library-complexity | 1 + 2024/01/31/coq-library-undecidability | 1 + 2024/01/31/ett-to-itt | 1 + 2024/01/31/frap | 1 + 2024/01/31/reification-by-parametricity | 1 + 2024/01/31/template-coq | 1 + 2024/01/SepLogicTypeclasses | 1 + 2024/01/bedrock | 1 + 2024/01/coq-a-la-carte-cpp20 | 1 + 2024/01/coq-elpi | 1 + 2024/01/coq-library-complexity | 1 + 2024/01/coq-library-undecidability | 1 + 2024/01/ett-to-itt | 1 + 2024/01/frap | 1 + 2024/01/reification-by-parametricity | 1 + 2024/01/template-coq | 1 + 22 files changed, 123 insertions(+) create mode 160000 2024/01/29/uttsolver create mode 160000 2024/01/31/SepLogicTypeclasses create mode 160000 2024/01/31/bedrock create mode 160000 2024/01/31/coq-a-la-carte-cpp20 create mode 160000 2024/01/31/coq-elpi create mode 160000 2024/01/31/coq-library-complexity create mode 160000 2024/01/31/coq-library-undecidability create mode 160000 2024/01/31/ett-to-itt create mode 160000 2024/01/31/frap create mode 160000 2024/01/31/reification-by-parametricity create mode 160000 2024/01/31/template-coq create mode 160000 2024/01/SepLogicTypeclasses create mode 160000 2024/01/bedrock create mode 160000 2024/01/coq-a-la-carte-cpp20 create mode 160000 2024/01/coq-elpi create mode 160000 2024/01/coq-library-complexity create mode 160000 2024/01/coq-library-undecidability create mode 160000 2024/01/ett-to-itt create mode 160000 2024/01/frap create mode 160000 2024/01/reification-by-parametricity create mode 160000 2024/01/template-coq diff --git a/.gitmodules b/.gitmodules index ab58c4bd..a9c7aca8 100644 --- a/.gitmodules +++ b/.gitmodules @@ -2756,3 +2756,105 @@ [submodule "2024/01/29/FreeSpec"] path = 2024/01/29/FreeSpec url = https://github.com/lthms/FreeSpec +[submodule "2024/01/29/uttsolver"] + path = 2024/01/29/uttsolver + url = https://github.com/samchrisinger/uttsolver +[submodule "2024/01/30/doctoral-thesis"] + path = 2024/01/30/doctoral-thesis + url = https://github.com/JasonGross/doctoral-thesis.git +[submodule "2024/01/30/bedrock"] + path = 2024/01/30/bedrock + url = https://github.com/mit-plv/bedrock.git +[submodule "2024/01/30/coq-tools"] + path = 2024/01/30/coq-tools + url = https://github.com/JasonGross/coq-tools +[submodule "2024/01/30/lob"] + path = 2024/01/30/lob + url = https://github.com/JasonGross/lob +[submodule "2024/01/30/coq-tactics"] + path = 2024/01/30/coq-tactics + url = https://github.com/JasonGross/coq-tactics +[submodule "2024/01/30/coq-scripts"] + path = 2024/01/30/coq-scripts + url = https://github.com/JasonGross/coq-scripts +[submodule "2024/01/30/slow-coq-examples"] + path = 2024/01/30/slow-coq-examples + url = https://github.com/JasonGross/slow-coq-examples +[submodule "2024/01/30/lob-paper"] + path = 2024/01/30/lob-paper + url = https://github.com/JasonGross/lob-paper +[submodule "2024/01/30/proviola-source"] + path = 2024/01/30/proviola-source + url = https://github.com/JasonGross/proviola-source +[submodule "2024/01/30/18.721"] + path = 2024/01/30/18.721 + url = https://github.com/JasonGross/18.721 +[submodule "2024/01/30/ct4s"] + path = 2024/01/30/ct4s + url = https://github.com/JasonGross/ct4s +[submodule "2024/01/30/neural-net-coq-interp"] + path = 2024/01/30/neural-net-coq-interp + url = https://github.com/JasonGross/neural-net-coq-interp +[submodule "2024/01/30/parsing-parses"] + path = 2024/01/30/parsing-parses + url = https://github.com/JasonGross/parsing-parses +[submodule "2024/01/30/adt-synthesis"] + path = 2024/01/30/adt-synthesis + url = https://github.com/JasonGross/adt-synthesis +[submodule "2024/01/30/ClosestPoints"] + path = 2024/01/30/ClosestPoints + url = https://github.com/JasonGross/ClosestPoints +[submodule "2024/01/30/variegated-reading-lists"] + path = 2024/01/30/variegated-reading-lists + url = https://github.com/danidiaz/variegated-reading-lists +[submodule "2024/01/30/Coda"] + path = 2024/01/30/Coda + url = https://github.com/Veridise/Coda +[submodule "2024/01/30/theory-pl-refinement-coq"] + path = 2024/01/30/theory-pl-refinement-coq + url = https://github.com/spgroup/theory-pl-refinement-coq +[submodule "2024/01/30/coq-ltac2-experiments"] + path = 2024/01/30/coq-ltac2-experiments + url = https://github.com/tchajed/coq-ltac2-experiments +[submodule "2024/01/30/coq-ltac-iter"] + path = 2024/01/30/coq-ltac-iter + url = https://github.com/gmalecha/coq-ltac-iter +[submodule "2024/01/30/ltac2-tutorial"] + path = 2024/01/30/ltac2-tutorial + url = https://github.com/tchajed/ltac2-tutorial +[submodule "2024/01/30/VplTactic"] + path = 2024/01/30/VplTactic + url = https://github.com/VERIMAG-Polyhedra/VplTactic +[submodule "2024/01/30/PolTac"] + path = 2024/01/30/PolTac + url = https://github.com/thery/PolTac +[submodule "2024/01/31/coq-library-complexity"] + path = 2024/01/31/coq-library-complexity + url = https://github.com/uds-psl/coq-library-complexity +[submodule "2024/01/31/coq-library-undecidability"] + path = 2024/01/31/coq-library-undecidability + url = https://github.com/uds-psl/coq-library-undecidability +[submodule "2024/01/31/bedrock"] + path = 2024/01/31/bedrock + url = https://github.com/mit-plv/bedrock/ +[submodule "2024/01/31/frap"] + path = 2024/01/31/frap + url = https://github.com/achlipala/frap +[submodule "2024/01/31/reification-by-parametricity"] + path = 2024/01/31/reification-by-parametricity + url = https://github.com/mit-plv/reification-by-parametricity +[submodule "2024/01/31/coq-elpi"] + path = 2024/01/31/coq-elpi + url = https://github.com/LPCIC/coq-elpi +[submodule "2024/01/31/coq-a-la-carte-cpp20"] + path = 2024/01/31/coq-a-la-carte-cpp20 + url = https://github.com/uds-psl/coq-a-la-carte-cpp20 +[submodule "2024/01/31/template-coq"] + path = 2024/01/31/template-coq + url = https://github.com/TheoWinterhalter/template-coq +[submodule "2024/01/31/SepLogicTypeclasses"] + path = 2024/01/31/SepLogicTypeclasses + url = https://github.com/normanrink/SepLogicTypeclasses +[submodule "2024/01/31/ett-to-itt"] + path = 2024/01/31/ett-to-itt + url = https://github.com/TheoWinterhalter/ett-to-itt diff --git a/2024/01/29/uttsolver b/2024/01/29/uttsolver new file mode 160000 index 00000000..225dcbe8 --- /dev/null +++ b/2024/01/29/uttsolver @@ -0,0 +1 @@ +Subproject commit 225dcbe88bb3252d1fa78b95bbe203f18efea011 diff --git a/2024/01/31/SepLogicTypeclasses b/2024/01/31/SepLogicTypeclasses new file mode 160000 index 00000000..509ddcbb --- /dev/null +++ b/2024/01/31/SepLogicTypeclasses @@ -0,0 +1 @@ +Subproject commit 509ddcbb0b69426f6384f99666f0d0540f79de26 diff --git a/2024/01/31/bedrock b/2024/01/31/bedrock new file mode 160000 index 00000000..e3ff3c2c --- /dev/null +++ b/2024/01/31/bedrock @@ -0,0 +1 @@ +Subproject commit e3ff3c2cba9976ac4351caaabb4bf7278bb0dcbd diff --git a/2024/01/31/coq-a-la-carte-cpp20 b/2024/01/31/coq-a-la-carte-cpp20 new file mode 160000 index 00000000..a400dad7 --- /dev/null +++ b/2024/01/31/coq-a-la-carte-cpp20 @@ -0,0 +1 @@ +Subproject commit a400dad7140e4a59cc1732ad56ee77839f850c2a diff --git a/2024/01/31/coq-elpi b/2024/01/31/coq-elpi new file mode 160000 index 00000000..6b98188b --- /dev/null +++ b/2024/01/31/coq-elpi @@ -0,0 +1 @@ +Subproject commit 6b98188bb72583d8f304d0c7d54def889b3ed87e diff --git a/2024/01/31/coq-library-complexity b/2024/01/31/coq-library-complexity new file mode 160000 index 00000000..14b5f413 --- /dev/null +++ b/2024/01/31/coq-library-complexity @@ -0,0 +1 @@ +Subproject commit 14b5f413d2fb7adecde79c5451b483f9a1af59a8 diff --git a/2024/01/31/coq-library-undecidability b/2024/01/31/coq-library-undecidability new file mode 160000 index 00000000..8880e198 --- /dev/null +++ b/2024/01/31/coq-library-undecidability @@ -0,0 +1 @@ +Subproject commit 8880e198bdc44cba1bd901f1fee701a95fc440ae diff --git a/2024/01/31/ett-to-itt b/2024/01/31/ett-to-itt new file mode 160000 index 00000000..b77534bf --- /dev/null +++ b/2024/01/31/ett-to-itt @@ -0,0 +1 @@ +Subproject commit b77534bf62673292da2139639f081cad4721a383 diff --git a/2024/01/31/frap b/2024/01/31/frap new file mode 160000 index 00000000..d9fb7fca --- /dev/null +++ b/2024/01/31/frap @@ -0,0 +1 @@ +Subproject commit d9fb7fca94af70c11e683ef2818d25cd850999eb diff --git a/2024/01/31/reification-by-parametricity b/2024/01/31/reification-by-parametricity new file mode 160000 index 00000000..d1bc17cf --- /dev/null +++ b/2024/01/31/reification-by-parametricity @@ -0,0 +1 @@ +Subproject commit d1bc17cf99a66e0268f655e28cdb375e712cd831 diff --git a/2024/01/31/template-coq b/2024/01/31/template-coq new file mode 160000 index 00000000..4f4b4fb6 --- /dev/null +++ b/2024/01/31/template-coq @@ -0,0 +1 @@ +Subproject commit 4f4b4fb6707ea5ad9d60e572671a1fdc9d950925 diff --git a/2024/01/SepLogicTypeclasses b/2024/01/SepLogicTypeclasses new file mode 160000 index 00000000..509ddcbb --- /dev/null +++ b/2024/01/SepLogicTypeclasses @@ -0,0 +1 @@ +Subproject commit 509ddcbb0b69426f6384f99666f0d0540f79de26 diff --git a/2024/01/bedrock b/2024/01/bedrock new file mode 160000 index 00000000..e3ff3c2c --- /dev/null +++ b/2024/01/bedrock @@ -0,0 +1 @@ +Subproject commit e3ff3c2cba9976ac4351caaabb4bf7278bb0dcbd diff --git a/2024/01/coq-a-la-carte-cpp20 b/2024/01/coq-a-la-carte-cpp20 new file mode 160000 index 00000000..a400dad7 --- /dev/null +++ b/2024/01/coq-a-la-carte-cpp20 @@ -0,0 +1 @@ +Subproject commit a400dad7140e4a59cc1732ad56ee77839f850c2a diff --git a/2024/01/coq-elpi b/2024/01/coq-elpi new file mode 160000 index 00000000..6b98188b --- /dev/null +++ b/2024/01/coq-elpi @@ -0,0 +1 @@ +Subproject commit 6b98188bb72583d8f304d0c7d54def889b3ed87e diff --git a/2024/01/coq-library-complexity b/2024/01/coq-library-complexity new file mode 160000 index 00000000..14b5f413 --- /dev/null +++ b/2024/01/coq-library-complexity @@ -0,0 +1 @@ +Subproject commit 14b5f413d2fb7adecde79c5451b483f9a1af59a8 diff --git a/2024/01/coq-library-undecidability b/2024/01/coq-library-undecidability new file mode 160000 index 00000000..8880e198 --- /dev/null +++ b/2024/01/coq-library-undecidability @@ -0,0 +1 @@ +Subproject commit 8880e198bdc44cba1bd901f1fee701a95fc440ae diff --git a/2024/01/ett-to-itt b/2024/01/ett-to-itt new file mode 160000 index 00000000..b77534bf --- /dev/null +++ b/2024/01/ett-to-itt @@ -0,0 +1 @@ +Subproject commit b77534bf62673292da2139639f081cad4721a383 diff --git a/2024/01/frap b/2024/01/frap new file mode 160000 index 00000000..d9fb7fca --- /dev/null +++ b/2024/01/frap @@ -0,0 +1 @@ +Subproject commit d9fb7fca94af70c11e683ef2818d25cd850999eb diff --git a/2024/01/reification-by-parametricity b/2024/01/reification-by-parametricity new file mode 160000 index 00000000..d1bc17cf --- /dev/null +++ b/2024/01/reification-by-parametricity @@ -0,0 +1 @@ +Subproject commit d1bc17cf99a66e0268f655e28cdb375e712cd831 diff --git a/2024/01/template-coq b/2024/01/template-coq new file mode 160000 index 00000000..4f4b4fb6 --- /dev/null +++ b/2024/01/template-coq @@ -0,0 +1 @@ +Subproject commit 4f4b4fb6707ea5ad9d60e572671a1fdc9d950925