Skip to content
This repository was archived by the owner on Nov 13, 2021. It is now read-only.

Commit ba6517a

Browse files
author
herbelin
committed
Intégration de micromega ("omicron" pour fourier et sa variante sur Z,
"micromega" et "sos" pour les problèmes non linéaires sous-traités à csdp); mise en place d'un cache pour pouvoir rejouer les preuves sans avoir besoin de csdp (pour l'instant c'est du bricolage, faudra affiner cela). git-svn-id: svn://scm.gforge.inria.fr/svn/coq/trunk@10947 85f007b7-540e-0410-9357-904b9bb8a0f7
1 parent 5346ff4 commit ba6517a

40 files changed

+23960
-368
lines changed

‎Makefile.build

+28-14
Original file line numberDiff line numberDiff line change
@@ -59,7 +59,7 @@ LOCALINCLUDES=-I config -I tools -I tools/coqdoc \
5959
-I scripts -I lib -I kernel -I kernel/byterun -I library \
6060
-I proofs -I tactics -I pretyping \
6161
-I interp -I toplevel -I parsing -I ide/utils -I ide \
62-
-I contrib/omega -I contrib/romega \
62+
-I contrib/omega -I contrib/romega -I contrib/micromega \
6363
-I contrib/ring -I contrib/dp -I contrib/setoid_ring \
6464
-I contrib/xml -I contrib/extraction \
6565
-I contrib/interface -I contrib/fourier \
@@ -163,12 +163,12 @@ coqlight: theories-light tools coqbinaries
163163

164164
states:: states/initial.coq
165165

166-
$(COQTOPOPT): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(USERTACCMX)
166+
$(COQTOPOPT): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN)
167167
$(SHOW)'COQMKTOP -o $@'
168168
$(HIDE)$(COQMKTOP) -opt $(OPTFLAGS) -o $@
169169
$(STRIP) $@
170170

171-
$(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(USERTACCMO)
171+
$(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN)
172172
$(SHOW)'COQMKTOP -o $@'
173173
$(HIDE)$(COQMKTOP) -top $(BYTEFLAGS) -o $@
174174

@@ -307,14 +307,13 @@ parsing/highparsing.cmxa: $(HIGHPARSING:.cmo=.cmx)
307307
$(SHOW)'OCAMLOPT -a -o $@'
308308
$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(HIGHPARSING:.cmo=.cmx)
309309

310-
tactics/hightactics.cma: $(HIGHTACTICS) $(USERTACCMO)
310+
tactics/hightactics.cma: $(HIGHTACTICS)
311311
$(SHOW)'OCAMLC -a -o $@'
312-
$(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(HIGHTACTICS) $(USERTACCMO)
312+
$(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(HIGHTACTICS)
313313

314-
tactics/hightactics.cmxa: $(HIGHTACTICS:.cmo=.cmx) $(USERTACCMO:.cmo=.cmx)
314+
tactics/hightactics.cmxa: $(HIGHTACTICS:.cmo=.cmx)
315315
$(SHOW)'OCAMLOPT -a -o $@'
316-
$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(HIGHTACTICS:.cmo=.cmx) \
317-
$(USERTACCMO:.cmo=.cmx)
316+
$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(HIGHTACTICS:.cmo=.cmx)
318317

319318
contrib/contrib.cma: $(CONTRIB)
320319
$(SHOW)'OCAMLC -a -o $@'
@@ -324,6 +323,20 @@ contrib/contrib.cmxa: $(CONTRIB:.cmo=.cmx)
324323
$(SHOW)'OCAMLOPT -a -o $@'
325324
$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(CONTRIB:.cmo=.cmx)
326325

326+
###########################################################################
327+
# Csdp to micromega special targets
328+
###########################################################################
329+
330+
ifeq ($(BEST),opt)
331+
bin/csdpcert$(EXE): $(CSDPCERTCMX)
332+
$(SHOW)'OCAMLOPT -o $@'
333+
$(HIDE)$(OCAMLOPT) $(OPTFLAGS) nums.cmxa -o $@ $(CSDPCERTCMX)
334+
else
335+
bin/csdpcert$(EXE): $(CSDPCERTCMO)
336+
$(SHOW)'OCAMLC -o $@'
337+
$(HIDE)$(OCAMLC) -custom $(BYTEFLAGS) nums.cma -o $@ $(CSDPCERTCMO)
338+
endif
339+
327340
###########################################################################
328341
# CoqIde special targets
329342
###########################################################################
@@ -343,12 +356,12 @@ coqide-byte: $(COQIDEBYTE) $(COQIDE)
343356
coqide-opt: $(COQIDEBYTE) $(COQIDEOPT) $(COQIDE)
344357
coqide-files: $(IDEFILES)
345358

346-
$(COQIDEOPT): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(USERTACCMX) ide/ide.cmxa
359+
$(COQIDEOPT): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) ide/ide.cmxa
347360
$(SHOW)'COQMKTOP -o $@'
348361
$(HIDE)$(COQMKTOP) -ide -opt $(OPTFLAGS) -o $@
349362
$(STRIP) $@
350363

351-
$(COQIDEBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(USERTACCMO) ide/ide.cma
364+
$(COQIDEBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) ide/ide.cma
352365
$(SHOW)'COQMKTOP -o $@'
353366
$(HIDE)$(COQMKTOP) -g -ide -top $(BYTEFLAGS) -o $@
354367

@@ -410,23 +423,23 @@ pcoq: pcoq-binaries pcoq-files
410423

411424
pcoq-binaries:: $(COQINTERFACE)
412425

413-
bin/coq-interface$(EXE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(USERTACCMO) $(INTERFACE)
426+
bin/coq-interface$(EXE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(INTERFACE)
414427
$(SHOW)'COQMKTOP -o $@'
415428
$(HIDE)$(COQMKTOP) -top $(BYTEFLAGS) -o $@ $(INTERFACE)
416429

417-
bin/coq-interface.opt$(EXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(USERTACCMX) $(INTERFACECMX)
430+
bin/coq-interface.opt$(EXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(INTERFACECMX)
418431
$(SHOW)'COQMKTOP -o $@'
419432
$(HIDE)$(COQMKTOP) -opt $(OPTFLAGS) -o $@ $(INTERFACECMX)
420433

421434
bin/parser$(EXE):$(LIBCOQRUN) $(PARSERCMO)
422435
$(SHOW)'OCAMLC -o $@'
423436
$(HIDE)$(OCAMLC) -custom -linkall $(BYTEFLAGS) -o $@ \
424-
dynlink.cma $(LIBCOQRUN) $(CMA) $(PARSERCMO)
437+
dynlink.cma nums.cma $(LIBCOQRUN) $(CMA) $(PARSERCMO)
425438

426439
bin/parser.opt$(EXE): $(LIBCOQRUN) $(PARSERCMX)
427440
$(SHOW)'OCAMLOPT -o $@'
428441
$(HIDE)$(OCAMLOPT) -linkall $(OPTFLAGS) -o $@ \
429-
$(LIBCOQRUN) $(CMXA) $(PARSERCMX)
442+
$(LIBCOQRUN) nums.cmxa $(CMXA) $(PARSERCMX)
430443

431444
pcoq-files:: $(INTERFACEVO) $(INTERFACERC)
432445

@@ -497,6 +510,7 @@ noreal: logic arith bool zarith qarith lists sets fsets relations \
497510

498511
contrib: $(CONTRIBVO) $(CONTRIBCMO)
499512
omega: $(OMEGAVO) $(OMEGACMO) $(ROMEGAVO) $(ROMEGACMO)
513+
micromega: $(MICROMEGAVO) $(MICROMEGACMO) $(CSDPCERT)
500514
ring: $(RINGVO) $(RINGCMO)
501515
setoid_ring: $(NEWRINGVO) $(NEWRINGCMO)
502516
dp: $(DPCMO)

‎Makefile.common

+33-14
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,8 @@ OTHERBINARIES:=$(COQMKTOPBYTE) $(COQCBYTE)
3838

3939
MINICOQ:=bin/minicoq$(EXE)
4040

41+
CSDPCERT:=bin/csdpcert
42+
4143
###########################################################################
4244
# tools
4345
###########################################################################
@@ -212,13 +214,8 @@ TOPLEVEL:=\
212214

213215
HIGHTACTICS:=\
214216
tactics/refine.cmo tactics/extraargs.cmo \
215-
tactics/extratactics.cmo tactics/eauto.cmo tactics/class_tactics.cmo
216-
217-
SPECTAC:= tactics/tauto.ml4 tactics/eqdecide.ml4
218-
USERTAC:= $(SPECTAC)
219-
220-
USERTACCMO:=$(USERTAC:.ml4=.cmo)
221-
USERTACCMX:=$(USERTAC:.ml4=.cmx)
217+
tactics/extratactics.cmo tactics/eauto.cmo tactics/class_tactics.cmo \
218+
tactics/tauto.cmo tactics/eqdecide.cmo
222219

223220
OMEGACMO:=\
224221
contrib/omega/omega.cmo contrib/omega/coq_omega.cmo \
@@ -228,6 +225,12 @@ ROMEGACMO:=\
228225
contrib/romega/const_omega.cmo \
229226
contrib/romega/refl_omega.cmo contrib/romega/g_romega.cmo
230227

228+
MICROMEGACMO:=\
229+
contrib/micromega/mutils.cmo contrib/micromega/vector.cmo \
230+
contrib/micromega/micromega.cmo contrib/micromega/mfourier.cmo \
231+
contrib/micromega/certificate.cmo \
232+
contrib/micromega/coq_micromega.cmo contrib/micromega/g_micromega.cmo
233+
231234
RINGCMO:=\
232235
contrib/ring/quote.cmo contrib/ring/g_quote.cmo \
233236
contrib/ring/ring.cmo contrib/ring/g_ring.cmo
@@ -302,7 +305,8 @@ SUBTACCMO:=contrib/subtac/subtac_utils.cmo contrib/subtac/eterm.cmo \
302305
RTAUTOCMO:=contrib/rtauto/proof_search.cmo contrib/rtauto/refl_tauto.cmo \
303306
contrib/rtauto/g_rtauto.cmo
304307

305-
CONTRIB:=$(OMEGACMO) $(ROMEGACMO) $(RINGCMO) $(NEWRINGCMO) $(DPCMO) $(FIELDCMO) \
308+
CONTRIB:=$(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) \
309+
$(RINGCMO) $(NEWRINGCMO) $(DPCMO) $(FIELDCMO) \
306310
$(FOURIERCMO) $(EXTRACTIONCMO) $(JPROVERCMO) $(XMLCMO) \
307311
$(CCCMO) $(FOCMO) $(SUBTACCMO) $(RTAUTOCMO) \
308312
$(FUNINDCMO)
@@ -325,7 +329,7 @@ LINKCMX:=$(LINKCMOCMXA:.cmo=.cmx)
325329
# objects known by the toplevel of Coq
326330
OBJSCMO:=$(CONFIG) $(LIBREP) $(KERNEL) $(LIBRARY) $(PRETYPING) $(INTERP) \
327331
$(PROOFS) $(PARSING) $(TACTICS) $(TOPLEVEL) $(HIGHPARSING) \
328-
$(HIGHTACTICS) $(USERTACMO) $(CONTRIB)
332+
$(HIGHTACTICS) $(CONTRIB)
329333

330334
COQIDECMO:=ide/utils/okey.cmo ide/utils/config_file.cmo \
331335
ide/utils/configwin_keys.cmo ide/utils/configwin_types.cmo \
@@ -375,6 +379,12 @@ PARSERCMX:= $(PARSERREQUIRESCMX) $(PARSERCODE:.cmo=.cmx)
375379

376380
INTERFACERC:= contrib/interface/vernacrc
377381

382+
CSDPCERTCMO:= contrib/micromega/mutils.cmo contrib/micromega/micromega.cmo \
383+
contrib/micromega/vector.cmo contrib/micromega/mfourier.cmo \
384+
contrib/micromega/certificate.cmo \
385+
contrib/micromega/sos.cmo contrib/micromega/csdpcert.cmo
386+
CSDPCERTCMX:= $(CSDPCERTCMO:.cmo=.cmx)
387+
378388
DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/printers.cma
379389

380390
COQDEPCMO:=config/coq_config.cmo tools/coqdep_lexer.cmo tools/coqdep.cmo
@@ -704,6 +714,15 @@ OMEGAVO:=$(addprefix contrib/omega/, \
704714
ROMEGAVO:=$(addprefix contrib/romega/, \
705715
ReflOmegaCore.vo ROmega.vo )
706716

717+
MICROMEGAVO:=$(addprefix contrib/micromega/, \
718+
CheckerMaker.vo Refl.vo \
719+
Env.vo RingMicromega.vo \
720+
EnvRing.vo VarMap.vo \
721+
OrderedRing.vo ZCoeff.vo \
722+
Micromegatac.vo ZMicromega.vo \
723+
QMicromega.vo RMicromega.vo \
724+
Tauto.vo )
725+
707726
RINGVO:=$(addprefix contrib/ring/, \
708727
LegacyArithRing.vo Ring_normalize.vo \
709728
LegacyRing_theory.vo LegacyRing.vo \
@@ -751,9 +770,9 @@ SUBTACVO:=$(addprefix theories/Program/, \
751770
RTAUTOVO:=$(addprefix contrib/rtauto/, \
752771
Bintree.vo Rtauto.vo )
753772

754-
CONTRIBVO:= $(OMEGAVO) $(ROMEGAVO) $(RINGVO) $(FIELDVO) $(XMLVO) \
755-
$(FOURIERVO) $(JPROVERVO) $(CCVO) $(FUNINDVO) $(SUBTACVO) \
756-
$(RTAUTOVO) $(RECDEFVO) $(NEWRINGVO) $(DPVO)
773+
CONTRIBVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \
774+
$(XMLVO) $(FOURIERVO) $(JPROVERVO) $(CCVO) $(FUNINDVO) \
775+
$(SUBTACVO) $(RTAUTOVO) $(RECDEFVO) $(NEWRINGVO) $(DPVO)
757776

758777
ALLVO:= $(INITVO) $(THEORIESVO) $(CONTRIBVO)
759778

@@ -808,12 +827,12 @@ STAGE1_TARGETS:= $(STAGE1) \
808827
STAGE2_TARGETS:=$(COQBINARIES) lib kernel byterun library proofs tactics \
809828
interp parsing pretyping highparsing toplevel hightactics \
810829
coqide-binaries coqide-byte coqide-opt $(COQIDEOPT) $(COQIDEBYTE) $(COQIDE) \
811-
pcoq-binaries $(COQINTERFACE) coqbinaries pcoq $(TOOLS) tools \
830+
pcoq-binaries $(COQINTERFACE) $(CSDPCERT) coqbinaries pcoq $(TOOLS) tools \
812831
printers $(MINICOQ) debug
813832
VO_TARGETS:=logic arith bool narith zarith qarith lists strings sets \
814833
fsets allfsets relations wellfounded ints reals allreals \
815834
setoids sorting natural integer rational numbers noreal \
816-
omega ring setoid_ring dp xml extraction field fourier jprover \
835+
omega micromega ring setoid_ring dp xml extraction field fourier jprover \
817836
funind cc programs subtac rtauto
818837
DOC_TARGETS:=doc doc-html doc-ps doc-pdf stdlib refman tutorial faq rectutorial
819838
STAGE3_TARGETS:=world install coqide coqide-files coq coqlib \

‎contrib/micromega/CheckerMaker.v

+13-7
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,16 @@
1-
(********************************************************************)
2-
(* *)
3-
(* Micromega: A reflexive tactics using the Positivstellensatz *)
4-
(* *)
5-
(* Frédéric Besson (Irisa/Inria) 2006 *)
6-
(* *)
7-
(********************************************************************)
1+
(************************************************************************)
2+
(* v * The Coq Proof Assistant / The Coq Development Team *)
3+
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4+
(* \VV/ **************************************************************)
5+
(* // * This file is distributed under the terms of the *)
6+
(* * GNU Lesser General Public License Version 2.1 *)
7+
(************************************************************************)
8+
(* *)
9+
(* Micromega: A reflexive tactic using the Positivstellensatz *)
10+
(* *)
11+
(* Frédéric Besson (Irisa/Inria) 2006-2008 *)
12+
(* *)
13+
(************************************************************************)
814

915
Require Import Setoid.
1016
Require Import Decidable.

0 commit comments

Comments
 (0)