update dockerfile and github actions

Signed-off-by: Avi Shinnar <shinnar@us.ibm.com>

Author: shinnar

.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'

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,12 +16,8 @@ RUN ["/bin/bash", "--login", "-c", "set -x \
   && opam clean -a -c -s --logs"]
 
 
-COPY --chown=coq:coq _CoqProject Makefile Makefile.rocq_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 coq ./formal_ml/coq
 
 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

@@ -14,10 +14,6 @@ depends: [
   "rocq-mathcomp-ssreflect"
   "coq-coquelicot"
   "coq-ext-lib" {<= "1.0.0"}
-  "ocamlbuild"
-  "base64"
-  "menhir"
-  "csv"
   "coq-coq2html" {with-doc}
 ]
 build: [[make]