@@ -8,6 +8,7 @@ section below.
88
99## Requirements
1010
11+ - Linux or macOS
1112- [ OCaml 4.07.1] ( https://ocaml.org )
1213- [ SerAPI 0.7.1] ( https://github.com/ejgallego/coq-serapi )
1314- [ Coq 8.10.2] ( https://coq.inria.fr/download )
@@ -16,7 +17,19 @@ section below.
1617
1718## Installation
1819
19- ### Installation of OCaml, Coq, and SerAPI
20+ You can install Roosterize from source code by cloning this GitHub
21+ repository and setting up the dependencies following steps 1 & 2.
22+ (Alternatively, you can download the a [ binary
23+ distribution] ( https://github.com/EngineeringSoftware/roosterize/releases )
24+ which already contains the Python dependencies, and then you only need
25+ step 1.)
26+
27+ ```
28+ git clone https://github.com/EngineeringSoftware/roosterize.git
29+ cd roosterize
30+ ```
31+
32+ ### 1. Installation of OCaml, Coq, and SerAPI
2033
2134We strongly recommend installing the required versions of OCaml, Coq,
2235and SerAPI via the [ OPAM package manager] ( https://opam.ocaml.org ) ,
@@ -35,93 +48,94 @@ opam pin add coq 8.10.2
3548opam pin add coq-serapi 8.10.0+0.7.1
3649```
3750
38- ### Installation of PyTorch and Python libraries
51+ ### 2. Installation of PyTorch and Python libraries
52+
53+ We strongly recommend installing the required versions of Python and
54+ PyTorch using [ Conda] ( https://docs.conda.io/en/latest/miniconda.html ) .
3955
40- We strongly recommend installing the required versions of Python and PyTorch
41- using [ Conda] ( https://docs.conda.io/en/latest/miniconda.html ) .
56+ To set up the Conda environment, use one of the following command
57+ suitable for your operating system and whether you want to use it on a
58+ CPU or GPU.
4259
43- First, create a Python 3.7 environment using Conda :
60+ - Linux, CPU :
4461```
45- conda create --name roosterize python=3.7 pip
46- conda activate roosterize
62+ conda env create --name roosterize --file conda-envs/cpu.yml
4763```
4864
49- Then, install PyTorch 1.1.0 by following the
50- [ official instructions] ( https://pytorch.org/get-started/previous-versions/#conda-5 ) ,
51- using the command suitable for your operating system and whether you want to use
52- it on a CPU or GPU. For example, the following command installs PyTorch for
53- CPU-only use on Linux or Windows:
65+ - Linux, GPU w/ CUDA 10.0:
5466```
55- conda install pytorch-cpu==1.1.0 torchvision-cpu==0.3.0 cpuonly -c pytorch
67+ conda env create --name roosterize --file conda-envs/gpu-cuda10.yml
5668```
57- Finally, install the required Python libraries:
69+
70+ - Linux, GPU w/ CUDA 9.0:
5871```
59- conda install configargparse nltk future seutil==0.4.12 six torchtext==0.4.0 tqdm==4.30.*
72+ conda env create --name roosterize --file conda-envs/gpu-cuda9.yml
6073```
6174
62- ### Installation of Roosterize and trained models
75+ - Mac, CPU:
76+ ```
77+ conda env create --name roosterize --file conda-envs/mac-cpu.yml
78+ ```
6379
64- To install Roosterize itself, clone the GitHub repository and enter the root directory :
80+ Finally, activate the Conda environment before using Roosterize :
6581```
66- git clone https://github.com/EngineeringSoftware/roosterize.git
67- cd roosterize
82+ conda activate roosterize
6883```
6984
70- Next, you need to obtain pre-trained models that capture
71- naming conventions. We have trained several models using our
72- [ corpus] [ math-comp-corpus ] , which follows the conventions
73- used in the [ Mathematical Components] [ math-comp-website ]
74- family of projects. These models are available for separate
75- [ download] [ models-link ] .
85+ ### Installation of trained models
86+
87+ Next, you need to obtain a pre-trained model that capture naming
88+ conventions. The default pre-trained model, which was trained using
89+ our [ corpus] [ math-comp-corpus ] and follows the conventions used in the
90+ [ Mathematical Components] [ math-comp-website ] family of projects, can
91+ be obtained by running the command:
7692
77- To use our pre-trained models, go to the Roosterize
78- root directory, and download and unpack the archive (` models.tgz ` ):
7993```
80- wget https://github.com/EngineeringSoftware/roosterize/releases/download/v8.10.0/models.tgz
81- tar xzf models.tgz
94+ ./bin/roosterize download_global_model
8295```
8396
84- [ models-link ] : https://github.com/EngineeringSoftware/roosterize/releases/download/v8.10.0/models.tgz
97+ The model will be downloaded to ` $HOME/.roosterize/ ` . To use a
98+ different model (that we [ released] [ latest-release ] or you trained),
99+ simply put it in ` $HOME/.roosterize/ ` .
85100
86101## Usage
87102
88103To use Roosterize on a Coq verification project, you first need to
89- build the Coq project using a command provided by the project
90- (usually ` make ` ). Then, at the root directory of
91- the Roosterize project repository, run the command
92- ```
93- python -m roosterize.main suggest_lemmas \
94- --project=$PATH_TO_PROJECT \
95- --serapi-options=$SERAPI_OPTIONS \
96- --model-dir=./models/roosterize-ta \
97- --output=./output
98- ```
99- where ` $PATH_TO_PROJECT ` should be replaced with the path to the
100- Coq project, and ` $SERAPI_OPTIONS ` should be replaced with the SerAPI
101- command line options for mapping logical paths to directories
102- (see [ SerAPI's documentation] [ serapi-faq-link ] ). For example,
103- if the logical path (inside Coq) for the project is ` Verified ` ,
104- you should set ` SERAPI_OPTIONS="-R $PATH_TO_PROJECT,Verified" ` .
105-
106- The above command extracts all lemmas from the project, uses Roosterize's
107- pre-trained model (at ` ./models/roosterize-ta ` ) to predict a lemma name
108- for each lemma, and finally prints the lemma name update suggestions,
109- i.e., the predicted lemma names that are different from to the existing ones.
110- Below is an example of printed suggestions:
111- ```
112- >>>>> Suggestions:
113- infotheo/ecc_classic/bch.v: infotheo.ecc_classic.bch.BCH.BCH_PCM_altP1 -> inde_F2
114- infotheo/ecc_classic/bch.v: infotheo.ecc_classic.bch.BCH.BCH_PCM_altP2 -> inde_mul
115- infotheo/ecc_classic/bch.v: infotheo.ecc_classic.bch.BCH.PCM_altP -> F2_eq0
116- ...
104+ build the Coq project using a command provided by the project (usually
105+ ` make ` ). Then, run this command to get the lemma name suggestions for
106+ the lemmas in a Coq document (.v file):
107+
108+ ```
109+ python -m roosterize.main suggest_naming --file=PATH_TO_FILE
117110```
118111
112+ Roosterize automatically infers the root directory of the project by
113+ finding ` _CoqProject ` , and reads ` _CoqProject ` to infer the SerAPI
114+ command line options (for mapping logical paths to directories, see
115+ [ SerAPI's documentation] [ serapi-faq-link ] ). If you don't have a
116+ ` _CoqProject ` file, you need to provide an additional argument
117+ ` --project_root=PATH_TO_PROJECT_ROOT ` .
118+
119+ <!-- where `$PATH_TO_PROJECT` should be replaced with the path to the -->
120+ <!-- Coq project, and `$SERAPI_OPTIONS` should be replaced with the SerAPI -->
121+ <!-- command line options for mapping logical paths to directories -->
122+ <!-- (see [SerAPI's documentation][serapi-faq-link]). For example, -->
123+ <!-- if the logical path (inside Coq) for the project is `Verified`, -->
124+ <!-- you should set `SERAPI_OPTIONS="-R $PATH_TO_PROJECT,Verified"`. -->
125+
126+ The above command extracts all lemmas from the file, uses the
127+ pre-trained model to generate likely lemma names for each lemma, and
128+ finally prints the lemma name update suggestions, i.e., the generated
129+ lemma names that are different from to the existing ones. See an
130+ [ example suggestion report] ( ./docs/example-suggestion.txt ) .
131+
119132For other usages and command line interfaces of Roosterize, please
120133check the help:
121134```
122135python -m roosterize.main help
123136```
124137
138+ [ latest-release ] : https://github.com/EngineeringSoftware/roosterize/releases/latest
125139[ serapi-faq-link ] : https://github.com/ejgallego/coq-serapi/blob/v8.10/FAQ.md#does-serapi-support-coqs-command-line-flags
126140
127141## Technique
0 commit comments