Skip to content

Commit bf46fce

Browse files
pengyuniepengyunie
committed
Including code.
1 parent a0929be commit bf46fce

File tree

135 files changed

+24171
-18
lines changed

Some content is hidden

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

135 files changed

+24171
-18
lines changed

‎.gitignore‎

Lines changed: 197 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,197 @@
1+
# Log file
2+
experiments.log
3+
4+
# Downloads files
5+
/_downloads/
6+
/models
7+
/models.tgz
8+
9+
### JetBrains
10+
/.idea/
11+
12+
# Covers JetBrains IDEs: IntelliJ, RubyMine, PhpStorm, AppCode, PyCharm, CLion, Android Studio and WebStorm
13+
# Reference: https://intellij-support.jetbrains.com/hc/en-us/articles/206544839
14+
15+
# User-specific stuff
16+
.idea/**/workspace.xml
17+
.idea/**/tasks.xml
18+
.idea/**/usage.statistics.xml
19+
.idea/**/dictionaries
20+
.idea/**/shelf
21+
22+
# Generated files
23+
.idea/**/contentModel.xml
24+
25+
# Sensitive or high-churn files
26+
.idea/**/dataSources/
27+
.idea/**/dataSources.ids
28+
.idea/**/dataSources.local.xml
29+
.idea/**/sqlDataSources.xml
30+
.idea/**/dynamic.xml
31+
.idea/**/uiDesigner.xml
32+
.idea/**/dbnavigator.xml
33+
34+
# Gradle
35+
.idea/**/gradle.xml
36+
.idea/**/libraries
37+
38+
# Gradle and Maven with auto-import
39+
# When using Gradle or Maven with auto-import, you should exclude module files,
40+
# since they will be recreated, and may cause churn. Uncomment if using
41+
# auto-import.
42+
# .idea/modules.xml
43+
# .idea/*.iml
44+
# .idea/modules
45+
46+
# CMake
47+
cmake-build-*/
48+
49+
# Mongo Explorer plugin
50+
.idea/**/mongoSettings.xml
51+
52+
# File-based project format
53+
*.iws
54+
55+
# IntelliJ
56+
out/
57+
58+
# mpeltonen/sbt-idea plugin
59+
.idea_modules/
60+
61+
# JIRA plugin
62+
atlassian-ide-plugin.xml
63+
64+
# Cursive Clojure plugin
65+
.idea/replstate.xml
66+
67+
# Crashlytics plugin (for Android Studio and IntelliJ)
68+
com_crashlytics_export_strings.xml
69+
crashlytics.properties
70+
crashlytics-build.properties
71+
fabric.properties
72+
73+
# Editor-based Rest Client
74+
.idea/httpRequests
75+
76+
# Android studio 3.1+ serialized cache file
77+
.idea/caches/build_file_checksums.ser
78+
79+
80+
### Python
81+
82+
# Byte-compiled / optimized / DLL files
83+
__pycache__/
84+
*.py[cod]
85+
*$py.class
86+
87+
# C extensions
88+
*.so
89+
90+
# Distribution / packaging
91+
.Python
92+
build/
93+
develop-eggs/
94+
dist/
95+
downloads/
96+
eggs/
97+
.eggs/
98+
lib/
99+
lib64/
100+
parts/
101+
sdist/
102+
var/
103+
wheels/
104+
pip-wheel-metadata/
105+
share/python-wheels/
106+
*.egg-info/
107+
.installed.cfg
108+
*.egg
109+
MANIFEST
110+
111+
# PyInstaller
112+
# Usually these files are written by a python script from a template
113+
# before PyInstaller builds the exe, so as to inject date/other infos into it.
114+
*.manifest
115+
*.spec
116+
117+
# Installer logs
118+
pip-log.txt
119+
pip-delete-this-directory.txt
120+
121+
# Unit test / coverage reports
122+
htmlcov/
123+
.tox/
124+
.nox/
125+
.coverage
126+
.coverage.*
127+
.cache
128+
nosetests.xml
129+
coverage.xml
130+
*.cover
131+
.hypothesis/
132+
.pytest_cache/
133+
134+
# Translations
135+
*.mo
136+
*.pot
137+
138+
# Django stuff:
139+
*.log
140+
local_settings.py
141+
db.sqlite3
142+
143+
# Flask stuff:
144+
instance/
145+
.webassets-cache
146+
147+
# Scrapy stuff:
148+
.scrapy
149+
150+
# Sphinx documentation
151+
docs/_build/
152+
153+
# PyBuilder
154+
target/
155+
156+
# Jupyter Notebook
157+
.ipynb_checkpoints
158+
159+
# IPython
160+
profile_default/
161+
ipython_config.py
162+
163+
# pyenv
164+
.python-version
165+
166+
# celery beat schedule file
167+
celerybeat-schedule
168+
169+
# SageMath parsed files
170+
*.sage.py
171+
172+
# Environments
173+
.env
174+
.venv
175+
env/
176+
venv/
177+
ENV/
178+
env.bak/
179+
venv.bak/
180+
181+
# Spyder project settings
182+
.spyderproject
183+
.spyproject
184+
185+
# Rope project settings
186+
.ropeproject
187+
188+
# mkdocs documentation
189+
/site
190+
191+
# mypy
192+
.mypy_cache/
193+
.dmypy.json
194+
dmypy.json
195+
196+
# Pyre type checker
197+
.pyre/

‎LICENSE‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
MIT License
2+
3+
Copyright (c) 2020-Present Roosterize
4+
5+
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
6+
7+
The above copyright notice and this permission notice (including the next paragraph) shall be included in all copies or substantial portions of the Software.
8+
9+
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

‎README.md‎

Lines changed: 55 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -3,23 +3,21 @@
33
Roosterize is a tool for suggesting lemma names in verification
44
projects that use the [Coq proof assistant](https://coq.inria.fr).
55

6-
<b>We are actively updating this repository and will make it ready by
7-
the end of May. Stay tuned!</b>
8-
96
## Requirements
107

118
- [OCaml 4.07.1](https://ocaml.org)
129
- [SerAPI 0.7.1](https://github.com/ejgallego/coq-serapi)
1310
- [Coq 8.10.2](https://coq.inria.fr/download)
14-
- [Python 3.7+](https://www.python.org)
11+
- [Python 3.7.7+](https://www.python.org)
1512
- [PyTorch 1.1.0](https://pytorch.org/get-started/previous-versions/#v110)
1613

1714
## Installation and usage
1815

16+
### Installation of OCaml, Coq, and SerAPI
17+
1918
We strongly recommend installing the required versions of OCaml, Coq,
2019
and SerAPI via the [OPAM package manager](https://opam.ocaml.org),
21-
version 2.0.6 or later. We recommend installing the required versions
22-
of Python and PyTorch using [Conda](https://docs.conda.io/en/latest/).
20+
version 2.0.6 or later.
2321

2422
To set up the OPAM-based OCaml environment, use:
2523
```
@@ -34,34 +32,73 @@ opam pin add coq 8.10.2
3432
opam pin add coq-serapi 8.10.0+0.7.1
3533
```
3634

37-
Then, install PyTorch following the instructions
35+
### Installation of Python and PyTorch
36+
37+
We recommend installing the required versions of Python and PyTorch
38+
using [Conda](https://docs.conda.io/en/latest/miniconda.html).
39+
40+
Then, install PyTorch by following the instructions
3841
[here](https://pytorch.org/get-started/previous-versions/#v110), using
39-
the correct installation command depending on your operating system,
40-
Python package manager, and whether you want to use it on CPU or GPU.
42+
the installation command suitable for your operating system, Python
43+
package manager, and whether you want to use it on a CPU or GPU.
4144

4245
Next, clone the Roosterize repository and enter the directory:
4346
```
4447
git clone https://github.com/EngineeringSoftware/roosterize.git
4548
cd roosterize
4649
```
4750

48-
To install other required Python libraries (`pip3` is included with
51+
To install other required Python libraries (`pip` is included with
4952
Python installation):
5053
```
51-
pip3 install -r requirements.txt
54+
pip install -r requirements.txt
55+
```
56+
57+
### Download pre-trained models
58+
59+
Roosterize's pre-trained models are available via this Google Drive
60+
[link](https://drive.google.com/file/d/1L0-BMOrP0WYX7L1bAhKRkJPLm7VPeMsE/view?usp=sharing).
61+
Download the file `models.tgz` from the link and put it under this
62+
directory, then uncompress the file:
63+
```
64+
tar xzf models.tgz
65+
```
66+
67+
### Usage
68+
69+
To use Roosterize on a Coq verification project, you need to first
70+
build and install the project with the command provided by the project
71+
(usually `make` followed by `make install`). Then, at the root directory of
72+
the project repository, run the command
73+
```
74+
python -m roosterize.main suggest_lemmas --project=$PATH_TO_PROJECT --serapi_options=$SERAPI_OPTIONS --model-dir=./models/roosterize-ta --output=./output
5275
```
76+
where `$PATH_TO_PROJECT` should be replaced with the path to the
77+
project, and `$SERAPI_OPTIONS` should be replaced with the SerAPI
78+
command line options for mapping logical paths to directories (see [SerAPI's
79+
documentation](https://github.com/ejgallego/coq-serapi/blob/v8.11/FAQ.md#does-serapi-support-coqs-command-line-flags)).
80+
For example, if the logical path (inside Coq) for the project is `Verified`,
81+
you should set `SERAPI_OPTIONS="-Q $PATH_TO_PROJECT,Verified"`.
5382

54-
To use Roosterize for suggesting lemma names in a Coq verification
55-
project using the pre-trained model (provided in this repository),
56-
where $PROJECT_PATH is the path to the project:
83+
The command extracts all lemmas from the project, uses Roosterize's
84+
pre-trained model (at `./models/roosterize-ta`) to predict a lemma name
85+
for each lemma, and finally prints the lemma name update suggestions,
86+
i.e., the predicted lemma names that are different from to the existing ones.
87+
Below is an example of printed suggestions:
5788
```
58-
python3 -m roosterize.main suggest_lemma_names --project_path=$PROJECT_PATH
89+
>>>>> Suggestions:
90+
infotheo/ecc_classic/bch.v: infotheo.ecc_classic.bch.BCH.BCH_PCM_altP1 -> inde_F2
91+
infotheo/ecc_classic/bch.v: infotheo.ecc_classic.bch.BCH.BCH_PCM_altP2 -> inde_mul
92+
infotheo/ecc_classic/bch.v: infotheo.ecc_classic.bch.BCH.PCM_altP -> F2_eq0
93+
infotheo/ecc_classic/bch.v: infotheo.ecc_classic.bch.BCH.PCM_alt_GRS -> P
94+
infotheo/ecc_classic/bch.v: infotheo.ecc_classic.bch.BCH_codebook -> map_P
95+
...
5996
```
6097

6198
For other usages and command line interfaces of Roosterize, please
62-
check the manual page:
99+
check the help:
63100
```
64-
python3 -m roosterize.main help
101+
python -m roosterize.main help
65102
```
66103

67104
## Technique
@@ -79,7 +116,7 @@ is serialized into the following tokens:
79116
(IDENT L1)(KEYWORD")")(KEYWORD :)(IDENT L1)(KEYWORD =i)(IDENT L2)
80117
(KEYWORD ->)(IDENT nerode)(IDENT L2)(IDENT N1)(KEYWORD .)))
81118
```
82-
and the corresponding elaborated term:
119+
and the corresponding elaborated term (simplified):
83120
```lisp
84121
(Prod (Name (Id char)) ... (Prod (Name (Id L1)) ...
85122
(Prod (Name (Id L2)) ... (Prod (Name (Id N1)) ...

‎configs/ChopKnlTree+ChopSynTree+attn+copy.json‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
{
2+
"batch_size": 16,
3+
"beam_search_max_len_factor": 1.5,
4+
"ckpt_keep_max": 3,
5+
"decoder": "rnn",
6+
"dim_decoder_hidden": 500,
7+
"dim_embed": 500,
8+
"dim_encoder_hidden": 500,
9+
"dropout": 0.5,
10+
"early_stopping_threshold": 3,
11+
"encoder": "brnn",
12+
"input_max": 3000,
13+
"inputs": "bsexpl1+fsexpl1",
14+
"learning_rate": 0.001,
15+
"max_grad_norm": 5,
16+
"output": "st",
17+
"rnn_num_layers": 1,
18+
"use_attn": true,
19+
"use_copy": true,
20+
"vocab_input_frequency_threshold": 5
21+
}

‎configs/Stmt+ChopKnlTree+ChopSynTree+attn+copy.json‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
{
2+
"batch_size": 16,
3+
"beam_search_max_len_factor": 1.5,
4+
"ckpt_keep_max": 3,
5+
"decoder": "rnn",
6+
"dim_decoder_hidden": 500,
7+
"dim_embed": 500,
8+
"dim_encoder_hidden": 500,
9+
"dropout": 0.5,
10+
"early_stopping_threshold": 3,
11+
"encoder": "brnn",
12+
"input_max": 3000,
13+
"inputs": "s+bsexpl1+fsexpl1",
14+
"learning_rate": 0.001,
15+
"max_grad_norm": 5,
16+
"output": "st",
17+
"rnn_num_layers": 2,
18+
"use_attn": true,
19+
"use_copy": true,
20+
"vocab_input_frequency_threshold": 5
21+
}

‎configs/Stmt+ChopKnlTree+attn+copy.json‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
{
2+
"batch_size": 32,
3+
"beam_search_max_len_factor": 1.5,
4+
"ckpt_keep_max": 3,
5+
"decoder": "rnn",
6+
"dim_decoder_hidden": 500,
7+
"dim_embed": 500,
8+
"dim_encoder_hidden": 500,
9+
"dropout": 0.5,
10+
"early_stopping_threshold": 3,
11+
"encoder": "brnn",
12+
"input_max": 3000,
13+
"inputs": "s+bsexpl1",
14+
"learning_rate": 0.001,
15+
"max_grad_norm": 5,
16+
"output": "st",
17+
"rnn_num_layers": 2,
18+
"use_attn": true,
19+
"use_copy": true,
20+
"vocab_input_frequency_threshold": 5
21+
}

0 commit comments

Comments
 (0)