Skip to content

Commit 4cbd9db

Browse files
shinnarshinnar
authored
Update to Rocq (#22)
Migrate code to Rocq 9 Signed-off-by: Avi Shinnar <shinnar@us.ibm.com> * Update dependencies Signed-off-by: Avi Shinnar <shinnar@us.ibm.com> * convert LM Signed-off-by: Avi Shinnar <shinnar@us.ibm.com> * Remove NeuralNetwork stuff Signed-off-by: Avi Shinnar <shinnar@us.ibm.com> * Update utils for new version of Rocq Signed-off-by: Avi Shinnar <shinnar@us.ibm.com> * remove ocaml extraction support Signed-off-by: Avi Shinnar <shinnar@us.ibm.com> * Remove FHE code Signed-off-by: Avi Shinnar <shinnar@us.ibm.com> * Remove Floatish and the dependencies on flocq and interval Signed-off-by: Avi Shinnar <shinnar@us.ibm.com> * Update ProbTheory for new version of Rocq Signed-off-by: Avi Shinnar <shinnar@us.ibm.com> * Update CertRL for new version of Rocq Signed-off-by: Avi Shinnar <shinnar@us.ibm.com> * progress Signed-off-by: Avi Shinnar <shinnar@us.ibm.com> * finish migration Signed-off-by: Avi Shinnar <shinnar@us.ibm.com> * update dockerfile and github actions Signed-off-by: Avi Shinnar <shinnar@us.ibm.com> * rename source directory coq->rocq Signed-off-by: Avi Shinnar <shinnar@us.ibm.com> * update README Signed-off-by: Avi Shinnar <shinnar@us.ibm.com> --------- Signed-off-by: Avi Shinnar <shinnar@us.ibm.com>
1 parent 1bfa4da commit 4cbd9db

153 files changed

Lines changed: 933 additions & 53560 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.github/workflows/build.yml‎

Lines changed: 6 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -10,12 +10,10 @@ jobs:
1010
runs-on: ubuntu-latest # container actions require GNU/Linux
1111
strategy:
1212
matrix:
13-
coq_container:
14-
# - coqorg/coq:8.12.2
15-
# - coqorg/coq:8.16.1-ocaml-4.13.1-flambda
16-
- coqorg/coq:8.18.0-ocaml-4.13.1-flambda
13+
rocq_container:
14+
- rocq/rocq-prover:9.0.1-ocaml-4.14.2-flambda
1715
container:
18-
image: ${{ matrix.coq_container }}
16+
image: ${{ matrix.rocq_container }}
1917
options: --user root
2018
steps:
2119
- uses: actions/checkout@v4
@@ -26,31 +24,8 @@ jobs:
2624
- name: ls
2725
run: ls -la .
2826
- name: Install Opam dependencies
29-
run: su coq -c 'eval $(opam env) && opam install --deps-only --with-test --with-doc -y -j 2 ./Formal_ML.opam'
27+
run: su rocq -c 'eval $(opam env) && opam install --deps-only --with-test --with-doc -y -j 2 ./Formal_ML.opam'
3028
- name: Build using Make
31-
run: su coq -c 'eval $(opam env) && make -kj 2'
29+
run: su rocq -c 'eval $(opam env) && make -kj 2'
3230
- name: Build documentation
33-
run: su coq -c 'eval $(opam env) && make -kj 2 doc'
34-
35-
# - uses: coq-community/docker-coq-action@v1
36-
# with:
37-
# opam_file: 'Formal_ML.opam'
38-
# coq_version: ${{ matrix.coq_version }}
39-
# ocaml_version: ${{ matrix.ocaml_version }}
40-
# # export: 'OPAMWITHTEST OPAMWITHDOC'
41-
# export: 'OPAMWITHDOC'
42-
# after_script: |
43-
# sudo cp -a $(opam config var Formal_ML:build)/documentation .
44-
# env:
45-
# OPAMWITHDOC: 'true'
46-
# OPAMWITHTEST: 'true'
47-
# - if: ${{ github.event_name == 'push' && github.ref == 'refs/heads/master' }}
48-
# name: deploy documentation
49-
# uses: JamesIves/github-pages-deploy-action@3.7.1
50-
# with:
51-
# ACCESS_TOKEN: ${{ secrets.ACCESS_TOKEN }}
52-
# REPOSITORY_NAME: FormalML/FormalML.github.io # the target repository
53-
# TARGET_FOLDER: main/documentation # target directory
54-
# BRANCH: main # The branch the action should deploy to.
55-
# FOLDER: documentation # The folder the action should deploy.
56-
# CLEAN: true # Automatically remove deleted files from the deploy branch
31+
run: su rocq -c 'eval $(opam env) && make -kj 2 doc'

‎.gitignore‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,9 +6,9 @@
66
*.aux
77
.coqdeps.d
88
.#*
9-
Makefile.coq
10-
Makefile.coq.conf
11-
.Makefile.coq.d
9+
Makefile.rocq
10+
Makefile.rocq.conf
11+
.Makefile.rocq.d
1212
extracted
1313
ocaml/_build
1414
bin

‎Dockerfile‎

Lines changed: 7 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,13 @@
1-
ARG coq_image="coqorg/coq:8.12.2"
2-
FROM ${coq_image}
1+
ARG rocq_image="rocq/rocq-prover:9.0.1"
2+
FROM ${rocq_image}
33

44
MAINTAINER Avi Shinnar "shinnar@us.ibm.com"
55

66
# needs to be a subdirectory to avoid causing problems with
7-
# the /home/coq/.opam directory (and probably other stuff)
8-
WORKDIR /home/coq
7+
# the /home/rocq/.opam directory (and probably other stuff)
8+
WORKDIR /home/rocq
99

10-
COPY --chown=coq:coq Formal_ML.opam ./formal_ml/
10+
COPY --chown=rocq:rocq Formal_ML.opam ./formal_ml/
1111

1212
RUN ["/bin/bash", "--login", "-c", "set -x \
1313
&& if [ -n \"${COMPILER_EDGE}\" ]; then opam switch ${COMPILER_EDGE} && eval $(opam env); fi \
@@ -16,13 +16,8 @@ RUN ["/bin/bash", "--login", "-c", "set -x \
1616
&& opam clean -a -c -s --logs"]
1717

1818

19-
COPY --chown=coq:coq breast-cancer-wisconsin.data breast-cancer-wisconsin.names ./formal_ml/
20-
COPY --chown=coq:coq _CoqProject Makefile Makefile.coq_modules ./formal_ml/
21-
COPY --chown=coq:coq coq ./formal_ml/coq
22-
COPY --chown=coq:coq ocaml ./formal_ml/ocaml
19+
COPY --chown=rocq:rocq _RocqProject Makefile Makefile.rocq_modules ./formal_ml/
20+
COPY --chown=rocq:rocq rocq ./formal_ml/rocq
2321

2422
RUN ["/bin/bash", "--login", "-c", "set -x && cd formal_ml && \
2523
make && make doc"]
26-
27-
# CMD ["/bin/bash", "--login", "-c", "set -x && cd formal_ml && \
28-
# make test"]

‎Formal_ML.opam‎

Lines changed: 4 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -9,25 +9,15 @@ homepage: "https://github.com/ibm/formalml"
99
bug-reports: "https://github.com/ibm/formalml/issues"
1010
depends: [
1111
"ocaml" {>= "4.07.0"}
12-
"coq" {>= "8.12.1"}
13-
"coq-mathcomp-ssreflect"
14-
"coq-mathcomp-algebra"
15-
"coq-mathcomp-algebra-tactics"
16-
"coq-mathcomp-real-closed"
17-
"coq-mathcomp-analysis" {< "1.0.0"}
18-
"coq-coquelicot" {= "3.3.1" }
19-
"coq-flocq" {>= "4.0.0" }
20-
"coq-interval" {>= "4.8.0"}
12+
"rocq-core" {>= "9.0.0"}
13+
"rocq-stdlib"
14+
"rocq-mathcomp-ssreflect"
15+
"coq-coquelicot"
2116
"coq-ext-lib" {<= "1.0.0"}
22-
"ocamlbuild"
23-
"base64"
24-
"menhir"
25-
"csv"
2617
"coq-coq2html" {with-doc}
2718
]
2819
build: [[make]
2920
[make "doc"] {with-doc}
30-
[make "test"] {with-test}
3121
]
3222
install: [make]
3323
dev-repo: "git+https://github.com/IBM/FormalML.git"

‎Makefile‎

Lines changed: 15 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -1,38 +1,29 @@
1-
# Contains the list of all the Coq modules
2-
include Makefile.coq_modules
1+
# Contains the list of all the Rocq modules
2+
include Makefile.rocq_modules
33

4-
COQ_FILES = $(addprefix coq/,$(MODULES:%=%.v))
4+
ROCQ_FILES = $(addprefix rocq/,$(MODULES:%=%.v))
55

6-
all: coq # ocaml
6+
all: rocq
77

8-
coq: Makefile.coq
9-
@$(MAKE) -f Makefile.coq
8+
rocq: Makefile.rocq
9+
@$(MAKE) -f Makefile.rocq
1010

11-
Makefile.coq: Makefile Makefile.coq_modules $(COQ_FILES)
12-
@coq_makefile -f _CoqProject $(COQ_FILES) -o Makefile.coq
11+
Makefile.rocq: Makefile Makefile.rocq_modules $(ROCQ_FILES)
12+
@rocq makefile -f _RocqProject $(ROCQ_FILES) -o Makefile.rocq
1313

14-
ocaml: coq
15-
@$(MAKE) -C ocaml native
14+
clean-rocq:
15+
- @$(MAKE) -f Makefile.rocq clean
1616

17-
clean-coq:
18-
- @$(MAKE) -f Makefile.coq clean
1917

20-
clean-ocaml:
21-
@$(MAKE) -C ocaml clean
22-
23-
24-
COQ_FILES_FOR_DOC = $(MODULES:%=%.v)
18+
ROCQ_FILES_FOR_DOC = $(MODULES:%=%.v)
2519
GLOB_FILES_FOR_DOC = $(MODULES:%=%.glob)
2620

27-
doc: coq
21+
doc: rocq
2822
mkdir -p documentation/html
2923
rm -f documentation/html/*.html
30-
cd coq && coq2html -d ../documentation/html -base FormalML -external http://coquelicot.saclay.inria.fr/html/ Coquelicot $(COQ_FILES_FOR_DOC) $(GLOB_FILES_FOR_DOC)
31-
32-
test: coq ocaml
33-
./bin/nnopt
24+
cd rocq && coq2html -d ../documentation/html -base FormalML -external http://coquelicot.saclay.inria.fr/html/ Coquelicot $(ROCQ_FILES_FOR_DOC) $(GLOB_FILES_FOR_DOC)
3425

35-
clean: clean-coq clean-ocaml
26+
clean: clean-rocq
3627
rm -rf documentation/html
3728

38-
.PHONY: all ocaml clean clean-coq coq test doc
29+
.PHONY: all clean clean-rocq rocq doc

Makefile.coq_modules renamed to Makefile.rocq_modules

Lines changed: 2 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,6 @@ UTILS = BasicUtils \
3030
ClassicUtils \
3131
CoquelicotAdd \
3232
ELim_Seq \
33-
ExtrFloatishIEEE \
3433
improper_integrals \
3534
Isomorphism \
3635
ListAdd \
@@ -46,24 +45,11 @@ UTILS = BasicUtils \
4645
StreamAdd \
4746
StreamLimits \
4847
Sums \
49-
nvector \
5048
Vector \
5149
PushNeg \
5250
DVector \
5351
Utils \
54-
Floatish/FloatishDef \
55-
Floatish/FloatishOps \
56-
Floatish/FloatishRealOps \
57-
Floatish/FloatishInterval \
58-
Floatish/FloatishIEEE \
59-
Floatish/FloatishReal \
60-
Floatish
61-
62-
NEURAL_NETWORKS = AxiomaticNormedRealVectorSpace \
63-
DefinedFunctions \
64-
derivlemmas \
65-
Gen_NN
66-
52+
derivlemmas
6753

6854
CERTRL = pmf_monad \
6955
qvalues \
@@ -122,20 +108,10 @@ QLEARN = \
122108
Tsitsiklis \
123109
jaakkola_vector
124110

125-
FHE = \
126-
nth_root \
127-
encode \
128-
encrypt \
129-
zp_prim_root \
130-
arith
131-
132111
MODULES = $(addprefix lib_utils/,$(QCERT_LIB_UTILS)) \
133112
$(addprefix CertRL/LM/,$(ELFIC_UTILS)) \
134113
$(addprefix utils/,$(UTILS)) \
135-
$(addprefix NeuralNetworks/,$(NEURAL_NETWORKS)) \
136114
$(addprefix ProbTheory/,$(PROB_THEORY)) \
137115
$(addprefix CertRL/,$(CERTRL)) \
138116
$(addprefix QLearn/,$(QLEARN)) \
139-
$(addprefix FHE/,$(FHE)) \
140-
API
141-
117+

‎README.md‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -8,15 +8,15 @@
88

99
## Getting Started
1010

11-
To compile the Coq code in this repository,
11+
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:
1212
- first install opam [opam (ocaml package manager)](https://opam.ocaml.org/).
13-
- Add support for coq ocaml repositories: `opam repo add coq-released --set-default https://coq.inria.fr/opam/released`.
14-
- If you want to create a local environment (switch), you can run `opam switch create nnsopt 4.07.0`.
15-
- Next, run `opam install . --deps-only`. This should install all the dependencies needed, including Coq.
13+
- Add support for rocq ocaml repositories: `opam repo add rocq-released https://rocq-prover.org/opam/released`
14+
- If you want to create a local environment (switch), you can run `opam switch create formalml 4.14.2`.
15+
- Next, run `opam install . --deps-only`. This should install all the dependencies needed, including Rocq.
1616
- Once the prerequisites are installed, run `make` to compile it.
1717

18-
Alternatively, the included Docker file can be built using Docker to compile the coq code in a suitable environment.
19-
`docker build --build-arg=coq_image="coqorg/coq:8.8.2" --pull -t nn_sopt .`
18+
Alternatively, the included Docker file can be built using Docker to compile the rocq code in a suitable environment.
19+
`docker build --pull -t formalml .`
2020

2121
## License
2222
This repository is distributed under the terms of the Apache 2.0 License, see LICENSE.txt.

‎_CoqProject‎

Lines changed: 0 additions & 1 deletion
This file was deleted.

‎_RocqProject‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
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"

0 commit comments

Comments
 (0)