Skip to content

Commit 0dd6f3d

Browse files
committed
update README
Signed-off-by: Avi Shinnar <shinnar@us.ibm.com>
1 parent cebb936 commit 0dd6f3d

1 file changed

Lines changed: 6 additions & 6 deletions

File tree

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.

0 commit comments

Comments
 (0)