Update to Rocq

.github/workflows/build.yml

@@ -10,12 +10,10 @@ jobs:
     runs-on: ubuntu-latest  # container actions require GNU/Linux
     strategy:
       matrix:
-        coq_container:
-#        - coqorg/coq:8.12.2
-#        - coqorg/coq:8.16.1-ocaml-4.13.1-flambda
-        - coqorg/coq:8.18.0-ocaml-4.13.1-flambda
+        rocq_container:
+        - rocq/rocq-prover:9.0.1-ocaml-4.14.2-flambda
     container:
-      image: ${{ matrix.coq_container }}
+      image: ${{ matrix.rocq_container }}
       options: --user root
     steps:
     - uses: actions/checkout@v4
@@ -26,31 +24,8 @@ jobs:
     - name: ls
       run: ls -la .
     - name: Install Opam dependencies
-      run: su coq -c 'eval $(opam env) && opam install --deps-only --with-test --with-doc -y -j 2 ./Formal_ML.opam'
+      run: su rocq -c 'eval $(opam env) && opam install --deps-only --with-test --with-doc -y -j 2 ./Formal_ML.opam'
     - name: Build using Make
-      run: su coq -c 'eval $(opam env) && make -kj 2'
+      run: su rocq -c 'eval $(opam env) && make -kj 2'
     - name: Build documentation
-      run: su coq -c 'eval $(opam env) && make -kj 2 doc'
-
-#       - uses: coq-community/docker-coq-action@v1
-#         with:
-#           opam_file: 'Formal_ML.opam'
-#           coq_version: ${{ matrix.coq_version }}
-#           ocaml_version: ${{ matrix.ocaml_version }}
-# #          export: 'OPAMWITHTEST OPAMWITHDOC'
-#           export: 'OPAMWITHDOC'
-#           after_script: |
-#             sudo cp -a $(opam config var Formal_ML:build)/documentation .
-#         env:
-#           OPAMWITHDOC: 'true'
-#          OPAMWITHTEST: 'true'
-      # - if: ${{ github.event_name == 'push' && github.ref == 'refs/heads/master' }}
-      #   name: deploy documentation
-      #   uses: JamesIves/github-pages-deploy-action@3.7.1
-      #   with:
-      #     ACCESS_TOKEN: ${{ secrets.ACCESS_TOKEN }}
-      #     REPOSITORY_NAME: FormalML/FormalML.github.io # the target repository
-      #     TARGET_FOLDER: main/documentation # target directory
-      #     BRANCH: main # The branch the action should deploy to.
-      #     FOLDER: documentation # The folder the action should deploy.
-      #     CLEAN: true # Automatically remove deleted files from the deploy branch
+      run: su rocq -c 'eval $(opam env) && make -kj 2 doc'

.gitignore

@@ -6,9 +6,9 @@
 *.aux
 .coqdeps.d
 .#*
-Makefile.coq
-Makefile.coq.conf
-.Makefile.coq.d
+Makefile.rocq
+Makefile.rocq.conf
+.Makefile.rocq.d
 extracted
 ocaml/_build
 bin

Dockerfile

@@ -1,13 +1,13 @@
-ARG coq_image="coqorg/coq:8.12.2"
-FROM ${coq_image}
+ARG rocq_image="rocq/rocq-prover:9.0.1"
+FROM ${rocq_image}
 
 MAINTAINER Avi Shinnar "shinnar@us.ibm.com"
 
 # needs to be a subdirectory to avoid causing problems with
-# the /home/coq/.opam directory (and probably other stuff)
-WORKDIR /home/coq
+# the /home/rocq/.opam directory (and probably other stuff)
+WORKDIR /home/rocq
 
-COPY --chown=coq:coq Formal_ML.opam ./formal_ml/
+COPY --chown=rocq:rocq Formal_ML.opam ./formal_ml/
 
 RUN ["/bin/bash", "--login", "-c", "set -x \
   && if [ -n \"${COMPILER_EDGE}\" ]; then opam switch ${COMPILER_EDGE} && eval $(opam env); fi \
@@ -16,13 +16,8 @@ RUN ["/bin/bash", "--login", "-c", "set -x \
   && opam clean -a -c -s --logs"]
 
 
-COPY --chown=coq:coq breast-cancer-wisconsin.data breast-cancer-wisconsin.names ./formal_ml/
-COPY --chown=coq:coq _CoqProject Makefile Makefile.coq_modules ./formal_ml/
-COPY --chown=coq:coq coq ./formal_ml/coq
-COPY --chown=coq:coq ocaml ./formal_ml/ocaml
+COPY --chown=rocq:rocq _RocqProject Makefile Makefile.rocq_modules ./formal_ml/
+COPY --chown=rocq:rocq rocq ./formal_ml/rocq
 
 RUN ["/bin/bash", "--login", "-c", "set -x && cd formal_ml && \
      make && make doc"]
-
-# CMD ["/bin/bash", "--login", "-c", "set -x && cd formal_ml && \
-#     make test"]

Formal_ML.opam

@@ -9,25 +9,15 @@ homepage: "https://github.com/ibm/formalml"
 bug-reports: "https://github.com/ibm/formalml/issues"
 depends: [
   "ocaml" {>= "4.07.0"}
-  "coq" {>= "8.12.1"}
-  "coq-mathcomp-ssreflect"
-  "coq-mathcomp-algebra"
-  "coq-mathcomp-algebra-tactics"
-  "coq-mathcomp-real-closed"
-  "coq-mathcomp-analysis" {< "1.0.0"}
-  "coq-coquelicot" {= "3.3.1" }
-  "coq-flocq" {>= "4.0.0" }
-  "coq-interval" {>= "4.8.0"}
+  "rocq-core" {>= "9.0.0"}
+  "rocq-stdlib"
+  "rocq-mathcomp-ssreflect"
+  "coq-coquelicot"
   "coq-ext-lib" {<= "1.0.0"}
-  "ocamlbuild"
-  "base64"
-  "menhir"
-  "csv"
   "coq-coq2html" {with-doc}
 ]
 build: [[make]
        [make "doc"] {with-doc}
-       [make "test"] {with-test}
        ]
 install: [make]
 dev-repo: "git+https://github.com/IBM/FormalML.git"

Makefile

@@ -1,38 +1,29 @@
-# Contains the list of all the Coq modules
-include Makefile.coq_modules
+# Contains the list of all the Rocq modules
+include Makefile.rocq_modules
 
-COQ_FILES = $(addprefix coq/,$(MODULES:%=%.v))
+ROCQ_FILES = $(addprefix rocq/,$(MODULES:%=%.v))
 
-all: coq # ocaml
+all: rocq
 
-coq: Makefile.coq
-	@$(MAKE) -f Makefile.coq
+rocq: Makefile.rocq
+	@$(MAKE) -f Makefile.rocq
 
-Makefile.coq: Makefile Makefile.coq_modules $(COQ_FILES)
-	@coq_makefile -f _CoqProject $(COQ_FILES) -o Makefile.coq
+Makefile.rocq: Makefile Makefile.rocq_modules $(ROCQ_FILES)
+	@rocq makefile -f _RocqProject $(ROCQ_FILES) -o Makefile.rocq
 
-ocaml: coq
-	@$(MAKE) -C ocaml native
+clean-rocq:
+	- @$(MAKE) -f Makefile.rocq clean
 
-clean-coq:
-	- @$(MAKE) -f Makefile.coq clean
 
-clean-ocaml:
-	@$(MAKE) -C ocaml clean
-
-
-COQ_FILES_FOR_DOC = $(MODULES:%=%.v)
+ROCQ_FILES_FOR_DOC = $(MODULES:%=%.v)
 GLOB_FILES_FOR_DOC = $(MODULES:%=%.glob)
 
-doc: coq
+doc: rocq
 	mkdir -p documentation/html
 	rm -f documentation/html/*.html
-	cd coq && coq2html -d ../documentation/html -base FormalML -external http://coquelicot.saclay.inria.fr/html/ Coquelicot $(COQ_FILES_FOR_DOC) $(GLOB_FILES_FOR_DOC)
-
-test: coq ocaml
-	./bin/nnopt
+	cd rocq && coq2html -d ../documentation/html -base FormalML -external http://coquelicot.saclay.inria.fr/html/ Coquelicot $(ROCQ_FILES_FOR_DOC) $(GLOB_FILES_FOR_DOC)
 
-clean: clean-coq clean-ocaml
+clean: clean-rocq
 	rm -rf documentation/html
 
-.PHONY: all ocaml clean clean-coq coq test doc
+.PHONY: all clean clean-rocq rocq doc

Makefile.coq_modules → Makefile.rocq_modules

@@ -30,7 +30,6 @@ UTILS = BasicUtils \
 	ClassicUtils \
 	CoquelicotAdd \
 	ELim_Seq \
-	ExtrFloatishIEEE \
 	improper_integrals \
 	Isomorphism \
 	ListAdd \
@@ -46,24 +45,11 @@ UTILS = BasicUtils \
 	StreamAdd \
 	StreamLimits \
 	Sums \
-	nvector \
 	Vector \
 	PushNeg \
 	DVector \
 	Utils \
-	Floatish/FloatishDef \
-	Floatish/FloatishOps \
-	Floatish/FloatishRealOps \
-	Floatish/FloatishInterval \
-	Floatish/FloatishIEEE \
-	Floatish/FloatishReal \
-	Floatish
-
-NEURAL_NETWORKS = AxiomaticNormedRealVectorSpace \
-		DefinedFunctions \
-		derivlemmas \
-		Gen_NN
-
+	derivlemmas
 
 CERTRL = pmf_monad \
 	qvalues \
@@ -122,20 +108,10 @@ QLEARN = \
 	Tsitsiklis \
 	jaakkola_vector
 
-FHE = \
-      nth_root \
-      encode \
-      encrypt \
-      zp_prim_root \
-      arith
-
 MODULES =  $(addprefix lib_utils/,$(QCERT_LIB_UTILS)) \
 	$(addprefix CertRL/LM/,$(ELFIC_UTILS)) \
 	$(addprefix utils/,$(UTILS)) \
-	$(addprefix NeuralNetworks/,$(NEURAL_NETWORKS)) \
 	$(addprefix ProbTheory/,$(PROB_THEORY)) \
 	$(addprefix CertRL/,$(CERTRL)) \
 	$(addprefix QLearn/,$(QLEARN)) \
-	$(addprefix FHE/,$(FHE)) \
-	API
-
+

README.md

@@ -8,15 +8,15 @@
 
  ## Getting Started
 
- To compile the Coq code in this repository,
+ To compile the [Rocq](https://rocq-prover.org/) (previously known as Coq) code in this repository, [Install Rocq](https://rocq-prover.org/install).  For example:
   - first install opam [opam (ocaml package manager)](https://opam.ocaml.org/).
-  - Add support for coq ocaml repositories: `opam repo add coq-released --set-default https://coq.inria.fr/opam/released`.
-  - If you want to create a local environment (switch), you can run `opam switch create nnsopt 4.07.0`.
-  - Next, run `opam install . --deps-only`.  This should install all the dependencies needed, including Coq.
+  - Add support for rocq ocaml repositories: `opam repo add rocq-released https://rocq-prover.org/opam/released`
+  - If you want to create a local environment (switch), you can run `opam switch create formalml 4.14.2`.
+  - Next, run `opam install . --deps-only`.  This should install all the dependencies needed, including Rocq.
   - Once the prerequisites are installed, run `make` to compile it.
 
- Alternatively, the included Docker file can be built using Docker to compile the coq code in a suitable environment.
- `docker build --build-arg=coq_image="coqorg/coq:8.8.2" --pull -t nn_sopt .`
+ Alternatively, the included Docker file can be built using Docker to compile the rocq code in a suitable environment.
+ `docker build --pull -t formalml .`
 
  ## License
  This repository is distributed under the terms of the Apache 2.0 License, see LICENSE.txt.

_RocqProject

@@ -0,0 +1 @@
+-R rocq FormalML -arg -set -arg "Warnings=+default,-ambiguous-path,-coercions,-hiding-delimiting-key,-overwriting-delimiting-key,-redundant-canonical-projection,-typechecker,-ssr-search-moved,-deprecated,-notation-overridden"