Skip to content

Commit 41f9350

Browse files
proux01proux01
committed
WIP
1 parent 2b4b485 commit 41f9350

25 files changed

+145
-95
lines changed

‎.nix/config.nix

+37-37
Original file line numberDiff line numberDiff line change
@@ -130,7 +130,7 @@ with builtins; with (import <nixpkgs> {}).lib;
130130
"coqutil" # -> overlay
131131
"kami" # -> overlay
132132
"riscvcoq" # -> overlay
133-
"CoLoR"
133+
"CoLoR" # -> overlay
134134
"bignums"
135135
"bignums-test"
136136
"coqprime"
@@ -140,14 +140,14 @@ with builtins; with (import <nixpkgs> {}).lib;
140140
"coq-elpi-test" # -> overlay
141141
"hierarchy-builder"
142142
"hierarchy-builder-test"
143-
"engine bench" # -> overlay
143+
"engine-bench" # -> overlay
144144
# TODO fcsl_pcm -> wait for MC 2 port
145145
"coq-ext-lib" # -> overlay
146146
"simple-io" # -> overlay
147147
"QuickChick" # -> overlay
148148
"quickchick-test" # -> overlay
149149
"menhir"
150-
"neural-net-coq-interp" # -> overlay
150+
"neural-net-coq-interp"
151151
"aac-tactics" # -> overlay
152152
"paco"
153153
"ITree" # -> overlay
@@ -198,55 +198,55 @@ with builtins; with (import <nixpkgs> {}).lib;
198198
stdlib-test.job = true;
199199
stdlib-refman-html.job = true;
200200
stdlib-html.job = true;
201-
# coq-elpi.override.version = "proux01:split_stdlib";
202-
# coq-elpi-test.override.version = "proux01:split_stdlib";
201+
coq-elpi.override.version = "proux01:split_stdlib"; # required overlay
202+
coq-elpi-test.override.version = "proux01:split_stdlib"; # required overlay
203203
# mathcomp.override.version = "proux01:split_stdlib";
204204
# mathcomp-test.override.version = "proux01:split_stdlib";
205-
tlc.override.version = "master-for-coq-ci"; # -> overlay
206-
# tlc.override.version = "proux01:split_stdlib";
205+
# tlc.override.version = "master-for-coq-ci"; # -> overlay
206+
tlc.override.version = "proux01:split_stdlib"; # require overlay
207207
# flocq.override.version = "split_stdlib";
208-
# coq-ext-lib.override.version = "split_stdlib";
209-
# aac-tactics.override.version = "split_stdlib";
210-
# coq-hammer-tactics.override.version = "proux01:split_stdlib";
211-
# coq-hammer.override.version = "proux01:split_stdlib";
208+
# coq-ext-lib.override.version = "split_stdlib"; # free overlay
209+
# aac-tactics.override.version = "split_stdlib"; # free overlay
210+
# coq-hammer-tactics.override.version = "proux01:split_stdlib"; # free overlay
211+
# coq-hammer.override.version = "proux01:split_stdlib"; # free overlay
212212
dpdgraph-test.override.version = "coq_19310";
213-
# math-classes.override.version = "split_stdlib";
213+
math-classes.override.version = "split_stdlib"; # required overlay
214214
# corn.override.version = "split_stdlib";
215-
# equations.override.version = "proux01:split_stdlib";
216-
# equations-test.override.version = "proux01:split_stdlib";
215+
equations.override.version = "proux01:split_stdlib"; # required overlay
216+
equations-test.override.version = "proux01:split_stdlib"; # required overlay
217217
# autosubst.override.version = "split_stdlib";
218218
# relation-algebra.override.version = "proux01:split_stdlib";
219219
# category-theory.override.version = "proux01:split_stdlib";
220220
# metacoq.override.version = "proux01:split_stdlib";
221-
# compcert.override.version = "proux01:split_stdlib";
222-
# simple-io.override.version = "proux01:split_stdlib";
221+
compcert.override.version = "proux01:split_stdlib"; # required overlay
222+
# simple-io.override.version = "proux01:split_stdlib"; # free overlay
223223
# QuickChick.override.version = "proux01:split_stdlib";
224224
# quickchick-test.override.version = "proux01:split_stdlib";
225-
# iris.override.version = "proux:split_stdlib";
226-
# vst.override.version = "proux01:split_stdlib";
227-
# smtcoq.override.version = "proux01:split_stdlib";
228-
# CoLoR.override.version = "proux01:split_stdlib";
229-
# ITree.override.version = "proux01:split_stdlib";
230-
# atbr.override.version = "split_stdlib";
231-
# stalmarck-tactic.override.version = "split_stdlib";
232-
# waterproof.override.version = "proux01:split_stdlib";
225+
# iris.override.version = "proux:split_stdlib"; # free overlay
226+
vst.override.version = "proux01:split_stdlib"; # required overlay
227+
# smtcoq.override.version = "proux01:split_stdlib"; # free overlay
228+
# CoLoR.override.version = "proux01:split_stdlib"; # free overlay
229+
# ITree.override.version = "proux01:split_stdlib"; # free overlay
230+
atbr.override.version = "split_stdlib"; # required overlay
231+
stalmarck-tactic.override.version = "split_stdlib"; # required overlay
232+
# waterproof.override.version = "proux01:split_stdlib"; # free overlay
233233
# smtcoq-trakt.override.version = "proux01:split_stdlib-trakt";
234234
# jasmin.override.version = "proux01:split_stdlib";
235-
# sf.override.version = "proux01:split_stdlib";
236-
# bbv.override.version = "proux01:split_stdlib";
237-
# paramcoq-test.override.version = "split_stdlib";
238-
# json.override.version = "proux01:split_stdlib";
239-
# neural-net-coq-interp.override.version = "proux01:split_stdlib";
240-
# engine-bench.override.version = "proux01:split_stdlib";
241-
# coq-performance-tests.override.version = "proux01:split_stdlib";
235+
sf.override.version = "proux01:split_stdlib"; # required overlay
236+
# bbv.override.version = "proux01:split_stdlib"; # free overlay
237+
# paramcoq-test.override.version = "split_stdlib"; # free overlay
238+
# json.override.version = "proux01:split_stdlib"; # free overlay
239+
# neural-net-coq-interp.override.version = "proux01:split_stdlib"; # free overlay
240+
# engine-bench.override.version = "proux01:split_stdlib"; # free overlay
241+
# coq-performance-tests.override.version = "proux01:split_stdlib"; # free overlay
242242
# coq-tools.override.version = "proux01:split_stdlib";
243-
# argosy.override.version = "proux01:split_stdlib";
244-
# perennial.override.version = "proux01:split_stdlib";
245-
# rewriter.override.version = "proux01:split_stdlib";
246-
# coqutil.override.version = "proux01:split_stdlib";
243+
# argosy.override.version = "proux01:split_stdlib"; # free overlay
244+
# perennial.override.version = "proux01:split_stdlib"; # free overlay
245+
rewriter.override.version = "proux01:split_stdlib"; # required overlay
246+
coqutil.override.version = "proux01:split_stdlib"; # required overlay
247247
# riscvcoq.override.version = "proux01:split_stdlib";
248-
# kami.override.version = "proux01:split_stdlib";
249-
# cross-crypto.override.version = "proux01:split_stdlib";
248+
kami.override.version = "proux01:split_stdlib"; # required overlay
249+
cross-crypto.override.version = "proux01:split_stdlib"; # required overlay
250250
# bedrock2.override.version = "proux01:split_stdlib";
251251
# rupicola.override.version = "proux01:split_stdlib";
252252
# fiat-crypto.override.version = "proux01:split_stdlib";

‎theories/Make.all

+28-28
Original file line numberDiff line numberDiff line change
@@ -503,55 +503,55 @@ Wellfounded/Lexicographic_Product.v
503503
Wellfounded/Lexicographic_Exponentiation.v
504504
nsatz/NsatzTactic.v
505505

506-
-Q Arith/All Stdlib.Arith.All.Arith
507-
-Q Arith/Base Stdlib.Arith.Base.Arith
506+
-Q Arith/All Stdlib.Arith.All.Stdlib.Arith
507+
-Q Arith/Base Stdlib.Arith.Base.Stdlib.Arith
508508
-Q Array Stdlib.Array
509509
-Q Bool Stdlib.Bool
510-
-Q Classes/All Stdlib.Classes.All.Classes
511-
-Q Classes/Arith Stdlib.Classes.Arith.Classes
512-
-Q Classes/Lists Stdlib.Classes.Lists.Classes
510+
-Q Classes/All Stdlib.Classes.All.Stdlib.Classes
511+
-Q Classes/Arith Stdlib.Classes.Arith.Stdlib.Classes
512+
-Q Classes/Lists Stdlib.Classes.Lists.Stdlib.Classes
513513
-Q Compat Stdlib.Compat
514514
-Q FSets Stdlib.FSets
515515
-Q Floats Stdlib.Floats
516516
-Q Lists Stdlib.Lists
517-
-Q Logic/Base Stdlib.Logic.Base.Logic
518-
-Q Logic/Classical Stdlib.Logic.Classical.Logic
519-
-Q Logic/Lists Stdlib.Logic.Lists.Logic
517+
-Q Logic/Base Stdlib.Logic.Base.Stdlib.Logic
518+
-Q Logic/Classical Stdlib.Logic.Classical.Stdlib.Logic
519+
-Q Logic/Lists Stdlib.Logic.Lists.Stdlib.Logic
520520
-Q MSets Stdlib.MSets
521521
-Q NArith Stdlib.NArith
522522
-Q Numbers Stdlib.Numbers
523523
-Q PArith Stdlib.PArith
524-
-Q Program/All Stdlib.Program.All.Program
525-
-Q QArith/All Stdlib.QArith.All.QArith
526-
-Q QArith/Base Stdlib.QArith.Base.QArith
527-
-Q QArith/Field Stdlib.QArith.Field.QArith
524+
-Q Program/All Stdlib.Program.All.Stdlib.Program
525+
-Q QArith/All Stdlib.QArith.All.Stdlib.QArith
526+
-Q QArith/Base Stdlib.QArith.Base.Stdlib.QArith
527+
-Q QArith/Field Stdlib.QArith.Field.Stdlib.QArith
528528
-Q Reals Stdlib.Reals
529-
-Q Relations/All Stdlib.Relations.All.Relations
529+
-Q Relations/All Stdlib.Relations.All.Stdlib.Relations
530530
-Q Sets Stdlib.Sets
531531
-Q Sorting Stdlib.Sorting
532532
-Q Streams Stdlib.Streams
533533
-Q Strings Stdlib.Strings
534-
-Q Structures/Def Stdlib.Structures.Def.Structures
535-
-Q Structures/Ex Stdlib.Structures.Ex.Structures
534+
-Q Structures/Def Stdlib.Structures.Def.Stdlib.Structures
535+
-Q Structures/Ex Stdlib.Structures.Ex.Stdlib.Structures
536536
-Q Unicode Stdlib.Unicode
537537
-Q Vectors Stdlib.Vectors
538538
-Q Wellfounded Stdlib.Wellfounded
539-
-Q ZArith/All Stdlib.ZArith.All.ZArith
540-
-Q ZArith/Base Stdlib.ZArith.Base.ZArith
541-
-Q ZArith/Ring Stdlib.ZArith.Ring.ZArith
539+
-Q ZArith/All Stdlib.ZArith.All.Stdlib.ZArith
540+
-Q ZArith/Base Stdlib.ZArith.Base.Stdlib.ZArith
541+
-Q ZArith/Ring Stdlib.ZArith.Ring.Stdlib.ZArith
542542
-Q btauto Stdlib.btauto
543543
-Q derive Stdlib.derive
544-
-Q extraction/All Stdlib.extraction.All.extraction
545-
-Q extraction/Base Stdlib.extraction.Base.extraction
544+
-Q extraction/All Stdlib.extraction.All.Stdlib.extraction
545+
-Q extraction/Base Stdlib.extraction.Base.Stdlib.extraction
546546
-Q funind Stdlib.funind
547-
-Q micromega/Int63 Stdlib.micromega.Int63.micromega
548-
-Q micromega/Lia Stdlib.micromega.Lia.micromega
549-
-Q micromega/Lqa Stdlib.micromega.Lqa.micromega
550-
-Q micromega/Lra Stdlib.micromega.Lra.micromega
551-
-Q micromega/Zify Stdlib.micromega.Zify.micromega
547+
-Q micromega/Int63 Stdlib.micromega.Int63.Stdlib.micromega
548+
-Q micromega/Lia Stdlib.micromega.Lia.Stdlib.micromega
549+
-Q micromega/Lqa Stdlib.micromega.Lqa.Stdlib.micromega
550+
-Q micromega/Lra Stdlib.micromega.Lra.Stdlib.micromega
551+
-Q micromega/Zify Stdlib.micromega.Zify.Stdlib.micromega
552552
-Q nsatz Stdlib.nsatz
553553
-Q omega Stdlib.omega
554554
-Q rtauto Stdlib.rtauto
555-
-Q setoid_ring/Q Stdlib.setoid_ring.Q.setoid_ring
556-
-Q setoid_ring/R Stdlib.setoid_ring.R.setoid_ring
557-
-Q setoid_ring/Z Stdlib.setoid_ring.Z.setoid_ring
555+
-Q setoid_ring/Q Stdlib.setoid_ring.Q.Stdlib.setoid_ring
556+
-Q setoid_ring/R Stdlib.setoid_ring.R.Stdlib.setoid_ring
557+
-Q setoid_ring/Z Stdlib.setoid_ring.Z.Stdlib.setoid_ring

‎theories/Make.arith

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
11
Arith/All/Arith.v
22

3-
-Q Arith/All Stdlib.Arith.All.Arith
3+
-Q Arith/All Stdlib.Arith.All.Stdlib.Arith

‎theories/Make.arith-base

+2-2
Original file line numberDiff line numberDiff line change
@@ -52,6 +52,6 @@ Numbers/Natural/Abstract/NLcm.v
5252
Numbers/Natural/Abstract/NOrder.v
5353
Classes/Arith/SetoidDec.v
5454

55-
-Q Arith/Base Stdlib.Arith.Base.Arith
55+
-Q Arith/Base Stdlib.Arith.Base.Stdlib.Arith
5656
-Q Numbers Stdlib.Numbers
57-
-Q Classes/Arith Stdlib.Classes.Arith.Classes
57+
-Q Classes/Arith Stdlib.Classes.Arith.Stdlib.Classes

‎theories/Make.classes

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,4 +4,4 @@ Classes/All/Morphisms_Relations.v
44
Classes/All/RelationPairs.v
55
Classes/All/SetoidClass.v
66

7-
-Q Classes/All Stdlib.Classes.All.Classes
7+
-Q Classes/All Stdlib.Classes.All.Stdlib.Classes

‎theories/Make.classical-logic

+1-1
Original file line numberDiff line numberDiff line change
@@ -14,4 +14,4 @@ Logic/Classical/ClassicalUniqueChoice.v
1414
Logic/Classical/SetoidChoice.v
1515
Logic/Classical/Diaconescu.v
1616

17-
-Q Logic/Classical Stdlib.Logic.Classical.Logic
17+
-Q Logic/Classical Stdlib.Logic.Classical.Stdlib.Logic

‎theories/Make.extraction

+1-1
Original file line numberDiff line numberDiff line change
@@ -20,4 +20,4 @@ extraction/All/ExtrOCamlInt63.v
2020
extraction/All/ExtrHaskellBasic.v
2121
extraction/All/ExtrHaskellNatInteger.v
2222

23-
-Q extraction/All Stdlib.extraction.All.extraction
23+
-Q extraction/All Stdlib.extraction.All.Stdlib.extraction

‎theories/Make.extraction-base

+1-1
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
11
extraction/Base/Extraction.v
22

3-
-Q extraction/Base Stdlib.extraction.Base.extraction
3+
-Q extraction/Base Stdlib.extraction.Base.Stdlib.extraction

‎theories/Make.field

+2-2
Original file line numberDiff line numberDiff line change
@@ -8,5 +8,5 @@ setoid_ring/Q/Field_tac.v
88
setoid_ring/Q/Rings_Q.v
99
setoid_ring/Q/Field.v
1010

11-
-Q QArith/Field Stdlib.QArith.Field.QArith
12-
-Q setoid_ring/Q Stdlib.setoid_ring.Q.setoid_ring
11+
-Q QArith/Field Stdlib.QArith.Field.Stdlib.QArith
12+
-Q setoid_ring/Q Stdlib.setoid_ring.Q.Stdlib.setoid_ring

‎theories/Make.lia

+2-2
Original file line numberDiff line numberDiff line change
@@ -23,5 +23,5 @@ micromega/Lia/ZCoeff.v
2323
micromega/Lia/RingMicromega.v
2424

2525
-Q omega Stdlib.omega
26-
-Q micromega/Zify Stdlib.micromega.Zify.micromega
27-
-Q micromega/Lia Stdlib.micromega.Lia.micromega
26+
-Q micromega/Zify Stdlib.micromega.Zify.Stdlib.micromega
27+
-Q micromega/Lia Stdlib.micromega.Lia.Stdlib.micromega

‎theories/Make.list

+2-2
Original file line numberDiff line numberDiff line change
@@ -8,5 +8,5 @@ Classes/Lists/EquivDec.v
88

99
-Q Lists Stdlib.Lists
1010
-Q Numbers Stdlib.Numbers
11-
-Q Logic/Lists Stdlib.Logic.Lists.Logic
12-
-Q Classes/Lists Stdlib.Classes.Lists.Classes
11+
-Q Logic/Lists Stdlib.Logic.Lists.Stdlib.Logic
12+
-Q Classes/Lists Stdlib.Classes.Lists.Stdlib.Classes

‎theories/Make.logic

+1-1
Original file line numberDiff line numberDiff line change
@@ -20,4 +20,4 @@ Logic/Base/EqdepFacts.v
2020
Logic/Base/Hurkens.v
2121
Logic/Base/RelationalChoice.v
2222

23-
-Q Logic/Base Stdlib.Logic.Base.Logic
23+
-Q Logic/Base Stdlib.Logic.Base.Stdlib.Logic

‎theories/Make.lqa

+1-1
Original file line numberDiff line numberDiff line change
@@ -2,4 +2,4 @@ micromega/Lqa/QMicromega.v
22
micromega/Lqa/Lqa.v
33
micromega/Lqa/DeclConstant.v
44

5-
-Q micromega/Lqa Stdlib.micromega.Lqa.micromega
5+
-Q micromega/Lqa Stdlib.micromega.Lqa.Stdlib.micromega

‎theories/Make.orders-ex

+1-1
Original file line numberDiff line numberDiff line change
@@ -9,4 +9,4 @@ Structures/Ex/OrderedTypeEx.v
99
Structures/Ex/OrdersAlt.v
1010
Structures/Ex/DecidableTypeEx.v
1111

12-
-Q Structures/Ex Stdlib.Structures.Ex.Structures
12+
-Q Structures/Ex Stdlib.Structures.Ex.Stdlib.Structures

‎theories/Make.primitive-int

+1-1
Original file line numberDiff line numberDiff line change
@@ -9,4 +9,4 @@ micromega/Int63/ZifyUint63.v
99
micromega/Int63/ZifySint63.v
1010

1111
-Q Numbers/Cyclic Stdlib.Numbers.Cyclic
12-
-Q micromega/Int63 Stdlib.micromega.Int63.micromega
12+
-Q micromega/Int63 Stdlib.micromega.Int63.Stdlib.micromega

‎theories/Make.program

+1-1
Original file line numberDiff line numberDiff line change
@@ -5,4 +5,4 @@ Program/All/WfExtensionality.v
55
Program/All/Program.v
66
Program/All/Combinators.v
77

8-
-Q Program/All Stdlib.Program.All.Program
8+
-Q Program/All Stdlib.Program.All.Stdlib.Program

‎theories/Make.qarith

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,5 +4,5 @@ QArith/All/QArith.v
44
Numbers/Q/DecimalQ.v
55
Numbers/Q/HexadecimalQ.v
66

7-
-Q QArith/All Stdlib.QArith.All.QArith
7+
-Q QArith/All Stdlib.QArith.All.Stdlib.QArith
88
-Q Numbers/Q Stdlib.Numbers.Number.Q

‎theories/Make.qarith-base

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,4 +3,4 @@ QArith/Base/Qminmax.v
33
QArith/Base/QOrderedType.v
44
QArith/Base/QArith_base.v
55

6-
-Q QArith/Base Stdlib.QArith.Base.QArith
6+
-Q QArith/Base Stdlib.QArith.Base.Stdlib.QArith

‎theories/Make.reals

+2-2
Original file line numberDiff line numberDiff line change
@@ -93,6 +93,6 @@ Numbers/R/DecimalR.v
9393
Numbers/R/HexadecimalR.v
9494

9595
-Q Reals Stdlib.Reals
96-
-Q setoid_ring/R Stdlib.setoid_ring.R.setoid_ring
97-
-Q micromega/Lra Stdlib.micromega.Lra.micromega
96+
-Q setoid_ring/R Stdlib.setoid_ring.R.Stdlib.setoid_ring
97+
-Q micromega/Lra Stdlib.micromega.Lra.Stdlib.micromega
9898
-Q Numbers/R Stdlib.Numbers.R

‎theories/Make.relations

+1-2
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,4 @@ Relations/All/Relation_Operators.v
22
Relations/All/Operators_Properties.v
33
Relations/All/Relations.v
44

5-
-Q Relations/All Stdlib.Relations.All.Relations
6-
5+
-Q Relations/All Stdlib.Relations.All.Stdlib.Relations

‎theories/Make.ring

+2-2
Original file line numberDiff line numberDiff line change
@@ -21,5 +21,5 @@ setoid_ring/Z/ArithRing.v
2121
setoid_ring/Z/NArithRing.v
2222
setoid_ring/Z/Ring_theory.v
2323

24-
-Q ZArith/Ring Stdlib.ZArith.Ring.ZArith
25-
-Q setoid_ring/Z Stdlib.setoid_ring.Z.setoid_ring
24+
-Q ZArith/Ring Stdlib.ZArith.Ring.Stdlib.ZArith
25+
-Q setoid_ring/Z Stdlib.setoid_ring.Z.Stdlib.setoid_ring

‎theories/Make.structures

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,4 +4,4 @@ Structures/Def/Orders.v
44
Structures/Def/OrdersFacts.v
55
Structures/Def/OrdersTac.v
66

7-
-Q Structures/Def Stdlib.Structures.Def.Structures
7+
-Q Structures/Def Stdlib.Structures.Def.Stdlib.Structures

‎theories/Make.zarith

+1-1
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@ btauto/Algebra.v
2222
btauto/Reflect.v
2323
btauto/Btauto.v
2424

25-
-Q ZArith/All Stdlib.ZArith.All.ZArith
25+
-Q ZArith/All Stdlib.ZArith.All.Stdlib.ZArith
2626
-Q Numbers/Natural/Binary Stdlib.Numbers.Natural.Binary
2727
-Q Numbers/Integer/Binary Stdlib.Numbers.Integer.Binary
2828
-Q Numbers/Integer/NatPairs Stdlib.Numbers.Integer.NatPairs

‎theories/Make.zarith-base

+1-1
Original file line numberDiff line numberDiff line change
@@ -38,4 +38,4 @@ ZArith/Base/Zeuclid.v
3838
ZArith/Base/Int.v
3939

4040
-Q Numbers/Integer/Abstract Stdlib.Numbers.Integer.Abstract
41-
-Q ZArith/Base Stdlib.ZArith.Base.ZArith
41+
-Q ZArith/Base Stdlib.ZArith.Base.Stdlib.ZArith

0 commit comments

Comments
 (0)