Clean up Makefile and README

README

@@ -60,88 +60,22 @@ APPLICATION STYLE "ftype"
 
  See Test.v for an explanation of how to use VCFloat in this style.
 
-------------------- Special Note: Flocq3/Flocq4 compatibility---------
-
-Between April 2022 and (estimated) October 2022, there is a
-Flocq compatibility issue for the installation of VCFloat.
-In the Coq Platform 2022.04, "Flocq" means Flocq 4.x
-and "Flocq3" means Flocq 3.x.  In that Platform release, CompCert 3.10
-is still using Flocq3, and therefore VST is still using Flocq3.
-
-Packages that must be compatible with VST must (therefore) also use Flocq3.
-Therefore in various files of VCFloat one will see (for example),
-Require Import IntervalFlocq3.Tactic.
-Require Import Flocq3.Core.
-
-The Coq Platform 2202.04 includes these packages (Flocq3 and IntervalFlocq3).
-
-As soon as the next release 3.11 of CompCert comes out, it will be
-a client of ordinary Flocq (meaning 4.x), as will VST, and the entire
-Flocq3 issue will disappear.
-
 ------------------------- Requirements Notes -------------------------
 
-VCFloat requires Coq 8.15 (but might work under Coq 8.14).
-
-VCFloat depends on the following further external libraries, accessed
-from opam, from the Coq Platform, or (deprecated method) automatically
-downloaded from their official sources and built during VCFloat's
-building process:
-
-- CompCert 3.10 (from AbsInt's GitHub at https://github.com/AbsInt/CompCert.git),
-  or from opam (but you don't need CompCert at all if you are using the "ftype" style, see above)
-
-- Ssreflect 1.5 or later, e.g. from opam
-
-- Mathematical Components (MathComp) 1.5 or later  (opam)
-
-- Flocq 3.4 (from INRIA GForge at
-  https://gforge.inria.fr/git/flocq/flocq.git, or from opam)
+VCFloat depends on Coq's Flocq and Interval packages.
 
-- Coq-Interval 4.3.0 (from INRIA GForge at
-  https://scm.gforge.inria.fr/anonscm/git/coq-interval/coq-interval.git,
-    or opam).
+See coq-vcfloat.opam to see which versions of Coq, coq-flocq, and coq-interval are needed.
 
-See ACKS for copyright and licensing information about those external
-libraries.
 
+To install:
 
-Usage method 1:
 Use the Coq Platform (https://github.com/coq/platform)
 to ensure that Coq has access to all the above-named packages.
-Then
- 1. cd into the vcfloat directory
+Very possibly, by early 2024 coq-vcfloat will be included in the Coq platform.
+
+If vcfloat is not already in the Coq Platform, then install the Coq platform, then:
+ 1. cd into the vcfloat/vcfloat directory
  2. make depend
  3. make
-
-Usage method 2: without using Coq Platform or opam
-(deprecated; not recently tested)
-Assuming that you already have a standard installation of Coq
-8.5beta2, GNU make, GNU autoconf, GNU automake, and git.
-
-  0. Fetch the external libraries mentioned above, by running the
-     following automatic script:
-
-     ./get_external_libs.sh
-
-     You can provide any further options that you want passed to the
-     `make' commands for Ssreflect and MathComp (e.g. -j)
-
-  1. Configure, by:
-
-     ./configure
-
-  2. Build, by:
-
-     make
-
-  After building, you do not need to move the files anywhere else
-  (and, by the way, `make install' does not work). The build system
-  automatically generates a ./run-coqide.sh script to edit the sources
-  with CoqIDE (if installed on your system), as well as local load
-  path configuration files for Emacs+ProofGeneral (if installed on
-  your system). If you want to compile code against VCFloat, you can
-  have a look at the autogenerated `coqopts' file, to grab the load
-  path options to pass to Coq and its relevant tools (coqc,
-  coq_makefile, etc.)
+ 4. make install
 

Test/Makefile

@@ -14,7 +14,7 @@ target: summation.vo
 	$(COQC) $(COQFLAGS) $*.v
 
 depend: 
-	$(COQDEP) $(COQFLAGS) *.v cverif/*.v > .depend
+	$(COQDEP) $(COQFLAGS) *.v > .depend
 
 all_clean: rm *.vo *.vok *.vos *.glob
 

coq-vcfloat.opam

@@ -1,4 +1,3 @@
-(* WARNING: This opam file has not been tested *)
 opam-version: "2.0"
 version: "dev"
 synopsis: "VCFloat: Floating Point Round-off Error Analysis"
@@ -12,7 +11,6 @@ authors: [
   "Richard Lethin"
 ]
 maintainer: "Andrew W. Appel <[email protected]>"
-homepage: "http://"
 dev-repo: "git+https://github.com/VeriNum/vcfloat"
 bug-reports: "https://github.com/VeriNum/vcfloat/issues"
 license: "LGPL-3.0-or-later"

vcfloat/Makefile

@@ -34,10 +34,17 @@ endif
 depend: 
 	$(COQDEP) $(COQFLAGS) *.v ../Test/*.v > .depend
 
+.depend:
+	$(error to build the .depend file: make depend)
+
 all_clean:
 	rm *.vo *.vok *.vos *.glob
 
--include .depend
+ifneq ($(MAKECMDGOALS),depend)
+ ifneq ($(MAKECMDGOALS),clean)
+  include .depend
+ endif
+endif
 
 clean:
 	rm -f {*,*/*}.{vo,vo?,glob}