Skip to content

Commit

Permalink
Merge branch 'coq8.11' into rpc
Browse files Browse the repository at this point in the history
  • Loading branch information
LasseBlaauwbroek committed Oct 19, 2023
2 parents 28c8b2a + 0d7a4ae commit 4a88aca
Show file tree
Hide file tree
Showing 24 changed files with 65 additions and 68 deletions.
6 changes: 3 additions & 3 deletions Dockerfile
Original file line number Diff line number Diff line change
Expand Up @@ -20,12 +20,12 @@ RUN $CONDA_EXE install -n python3.10 -c conda-forge capnproto
RUN sudo apt-get update
RUN sudo apt-get --yes install graphviz pkg-config libev-dev libxxhash-dev cmake build-essential

COPY --chown=coq:coq . coq-tactician-reinforce
COPY --chown=coq:coq . coq-tactician-api

WORKDIR coq-tactician-reinforce
WORKDIR coq-tactician-api

RUN eval $(opam env) && opam update \
&& opam install --assume-depexts -t ./coq-tactician-reinforce.opam -y
&& opam install --assume-depexts -t ./coq-tactician-api.opam -y

RUN pip install .

Expand Down
6 changes: 3 additions & 3 deletions Dockerfile_base
Original file line number Diff line number Diff line change
Expand Up @@ -24,10 +24,10 @@ RUN sudo apt-get --yes install graphviz capnproto libcapnp-dev pkg-config libev-

# opam level project dependencies

COPY --chown=coq:coq . coq-tactician-reinforce
COPY --chown=coq:coq . coq-tactician-api
USER coq
WORKDIR /home/coq/coq-tactician-reinforce
WORKDIR /home/coq/coq-tactician-api
RUN eval $(opam env) \
&& opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev -y
RUN eval $(opam env) \
&& opam install -y -t --deps-only --solver=mccs ./coq-tactician-reinforce.opam
&& opam install -y -t --deps-only --solver=mccs ./coq-tactician-api.opam
22 changes: 11 additions & 11 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -14,8 +14,8 @@ component that should be installed through the Pip package manager. Additionally
The simplest and most reliable way to install these packages is through Conda. This repository provides a
`environment.yml` file with the required Conda dependencies. To set it up, follow these commands:
```
git clone --recurse-submodules git@github.com:coq-tactician/coq-tactician-reinforce.git # Clone this repo
cd coq-tactician-reinforce
git clone --recurse-submodules git@github.com:coq-tactician/coq-tactician-api.git # Clone this repo
cd coq-tactician-api
conda env create -f environment.yml
conda activate tactician
export CPATH="$CONDA_PREFIX:$CPATH" # Needed by cmake to find conda headers
Expand Down Expand Up @@ -67,8 +67,8 @@ about all the options).
A tactic prediction server acting as an oracle, retrieving it's information from a dataset
- `pytact-fake-coq [-h] (--tcp TCP_LOCATION | --stdin EXECUTABLE) data`
A fake Coq client that connects to a prediction server and feeds it a stream of previously recorded messages.
- `pytact-prover`: A dummy example client that interfaces with Coq and Tactician for reinforcement-learning-style
communication. To learn how to interface Coq and Tactician with this client, see the sections below.
- `pytact-prover`: A dummy example client that interfaces with Coq and Tactician for proof exploration
driven by the client. To learn how to interface Coq and Tactician with this client, see the sections below.

## Usage of the Coq plugin

Expand Down Expand Up @@ -136,16 +136,16 @@ At this point, you have the following commands available which will interact wit
- `Set Tactician Autocache` will automatically execute `Tactician Neural Cache` on each command. This is an
experimental option, and there may be some overhead associated with this.

## Reinforcement interaction
## Client-based proof exploration

Finally, the command `Reinforce.` will initiate a reinforcement session. An example of this is available in
Finally, the command `Explore.` will initiate a proof exploration session. An example of this is available in
[TestReinforceStdin.v](pytact/tests/TestReinforceStdin.v).
To do this, you need to have a python client running. An example is available in the `pytact-prover` executable.
To see how it works, run
```
pytact-prover --pdfsequence --pdfname test
```
This will execute a dummy proof through the reinforcement learning interface. Visualizations of each proof state
This will execute a dummy proof through the proof exploration interface. Visualizations of each proof state
are available in `test<n>.pdf`.
optionally `--file` option to point to a source Coq `.v` file.
Also with `--interactive` option the innteractive shell appears where you can
Expand All @@ -161,10 +161,10 @@ in the `generate-dataset` branch. The procedure to generate the dataset is as fo
```
opam switch create tacgen --empty
```
2. Install coq-tactician-reinforce generate-dataset
2. Install coq-tactician-api generate-dataset
```
git clone -b generate-dataset --recurse-submodules git@github.com:coq-tactician/coq-tactician-reinforce.git
cd coq-tactician-reinforce
git clone -b generate-dataset --recurse-submodules git@github.com:coq-tactician/coq-tactician-api.git
cd coq-tactician-api
opam install .
tactician inject # you can answer 'no' to recompiling
opam install coq-tactician-stdlib --keep-build-dir # make sure that you have the coq-extra-dev repo enabled
Expand Down Expand Up @@ -205,7 +205,7 @@ Debian.10/opam 2.0.9/coq 8.11.2/ocaml-variants-4.11.2+flambda.

The layer defined by `Dockerfile_base` adds `conda/python 3.9`,
`capnp` library and all opam package dependencies requested by the
coq-tactician-reinforce (including the opam package defined in git
coq-tactician-api (including the opam package defined in git
submodule `coq-tactician`).

The image defined by `Dockerfile_base` can be updated by maintainers (currently Vasily) by
Expand Down
7 changes: 3 additions & 4 deletions coq-tactician-reinforce.opam → coq-tactician-api.opam
Original file line number Diff line number Diff line change
@@ -1,12 +1,11 @@
# This file is generated by dune, edit dune-project instead
opam-version: "2.0"
synopsis: "Reinforcement learning for Tactician"
synopsis: "An API exposing Coq's web of formal knowledge to external agents"
description: ""
maintainer: ["Lasse Blaauwbroek <lasse@blaauwbroek.eu>"]
authors: ["Lasse Blaauwbroek <lasse@blaauwbroek.eu>"]
homepage: "https://coq-tactician.github.io"
bug-reports:
"https://github.com/coq-tactician/coq-tactician-reinforce/issues"
bug-reports: "https://github.com/coq-tactician/coq-tactician-api/issues"
build: [
["dune" "subst"] {dev}
[
Expand All @@ -23,7 +22,7 @@ build: [
]
["dune" "install" "-p" name "--create-install-files" name]
]
dev-repo: "git+https://github.com/coq-tactician/coq-tactician-reinforce.git"
dev-repo: "git+https://github.com/coq-tactician/coq-tactician-api.git"
pin-depends: [
[
"coq-tactician.8.11.dev"
Expand Down
File renamed without changes.
2 changes: 1 addition & 1 deletion datasets/current/README
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ For Python, a library called PyTactician (TODO: Link to Pypi and documentation)
is provided that allows for easy and efficient access to the data. It includes
software to visualize the dataset, a sanity checker for the dataset, an example
prediction server that interfaces with Coq, an Oracle prediction server and
a client for the reinforcement learning component.
an example proof exploration client.

The data in this archive is represented as a SquashFS image 'dataset.squ'.
If you are using the PyTactician library, you can load the dataset by pointing
Expand Down
2 changes: 1 addition & 1 deletion datasets/current/make_dataset.sh
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,7 @@ OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
SOFTWARE.
EOF

cp $(opam var prefix)/share/coq-tactician-reinforce/graph_api.capnp $datasetname/meta/graph_api.capnp
cp $(opam var prefix)/share/coq-tactician-api/graph_api.capnp $datasetname/meta/graph_api.capnp

for f in $scriptpath/stage*.sh; do
base=$(basename $f)
Expand Down
2 changes: 1 addition & 1 deletion datasets/current/stage1.sh
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
opam init --root=./opam-root --no-setup --bare
opam switch create . --empty --root=./opam-root --repos=custom-archive=git+https://github.com/LasseBlaauwbroek/custom-archive.git,coq-extra-dev=https://coq.inria.fr/opam/extra-dev,coq-core-dev=https://coq.inria.fr/opam/core-dev,coq-released=https://coq.inria.fr/opam/released,default
eval $(opam env --root=./opam-root --set-root)
time opam install --keep-build-dir --yes --assume-depext ./coq-tactician-reinforce/coq-tactician-reinforce.opam lwt.4.5.0 ocaml-base-compiler.4.09.1 js_of_ocaml.3.9.0 menhir.20190924
time opam install --keep-build-dir --yes --assume-depext ./coq-tactician-api/coq-tactician-api.opam lwt.4.5.0 ocaml-base-compiler.4.09.1 js_of_ocaml.3.9.0 menhir.20190924
tactician inject
opam switch export opam-stage1 --freeze
8 changes: 4 additions & 4 deletions dune-project
Original file line number Diff line number Diff line change
@@ -1,15 +1,15 @@
(lang dune 2.9)
(using dune_site 0.1)
(name coq-tactician-reinforce)
(name coq-tactician-api)
(using coq 0.3)
(generate_opam_files true)

(source (github coq-tactician/coq-tactician-reinforce))
(source (github coq-tactician/coq-tactician-api))
(homepage "https://coq-tactician.github.io")
(authors "Lasse Blaauwbroek <lasse@blaauwbroek.eu>")
(maintainers "Lasse Blaauwbroek <lasse@blaauwbroek.eu>")

(package
(name coq-tactician-reinforce)
(synopsis "Reinforcement learning for Tactician")
(name coq-tactician-api)
(synopsis "An API exposing Coq's web of formal knowledge to external agents")
(description ""))
17 changes: 9 additions & 8 deletions graph_api.capnp
Original file line number Diff line number Diff line change
Expand Up @@ -9,12 +9,13 @@
# 1. A schema for graph-based dataset exported from Coq. The entry-point for this is the `Dataset`
# struct. That is, every file in the dataset contains a message conforming to this struct.
#
# 2. A communication protocol for reinforcement learning. Depending on who initiates the learning
# (Coq or the learning agent), the entry-point for this is respectively the `PushReinforce` or
# the `PullReinforce` interface.
# 2. A communication protocol for proof synthesis with Tactician. There are two protocols for this:
# - A simple, linear message exchange protocol, specified by the `PredictionProtocol` struct.
# - An RPC based protocol, specified by the `PredictionServer` interface.
#
# 2. A communication protocol for proof exploration by a client. Proof exploration is started through
# the `explore` function of the `PredictionServer` interface.
#
# 3. A communication protocol for proof synthesis with Tactician. The entry-point of this
# protocol is the `PredictionProtocol` struct.
#
# All these three entry-points share a common base, which encodes the notion of graphs, terms,
# tactics and more.
Expand Down Expand Up @@ -574,7 +575,7 @@ struct PredictionProtocol {
######################################################################################################

struct Exception {
# A list of things that can go wrong during reinforcement learning.
# A list of things that can go wrong.
union {
noSuchTactic @0 :Void;
mismatchedArguments @1 :Void;
Expand Down Expand Up @@ -619,8 +620,8 @@ interface PredictionServer {
addGlobalContext @0 GlobalContextAddition -> ();
requestPrediction @1 PredictionRequest -> (predictions :List(Prediction));
checkAlignment @2 () -> (unalignedTactics :List(TacticId), unalignedDefinitions :List(Node));
reinforce @3 (result :ExecutionResult);
# An interface allowing a reinforcement learning session to be initiated by Coq. In this case, Coq decides
explore @3 (result :ExecutionResult);
# An interface allowing a proof exploration session to be initiated by Coq. In this case, Coq decides
# what lemma should be proved and immediately presents the agent with the initial execution result.
}

Expand Down
6 changes: 3 additions & 3 deletions pytact/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ communication protocol. Any PyTactician version `x.y` is compatible with the com

Binary wheels are provided for Linux and MacOS. On those platforms you can install by executing
`pip install pytactician`. If you need to install from source, you need to have Capt'n Proto >= 0.8 installed
on your system. See the main repo [README](https://github.com/coq-tactician/coq-tactician-reinforce#prerequisites)
on your system. See the main repo [README](https://github.com/coq-tactician/coq-tactician-api#prerequisites)
for more details on prerequisites.

## Usage
Expand All @@ -28,8 +28,8 @@ about all the options).
A tactic prediction server acting as an oracle, retrieving it's information from a dataset
- `pytact-fake-coq [-h] (--tcp TCP_LOCATION | --stdin EXECUTABLE) data`
A fake Coq client that connects to a prediction server and feeds it a stream of previously recorded messages.
- `pytact-prover`: A dummy example client that interfaces with Coq and Tactician for reinforcement-learning-style
communication. To learn how to interface Coq and Tactician with this client, see the sections below.
- `pytact-prover`: A dummy example client that interfaces with Coq and Tactician for proof exploration
driven by the client.

## Documentation

Expand Down
8 changes: 4 additions & 4 deletions pytact/prover.py
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
"""
a test of connection to coq-tactician-reinforce
a test of connection to coq-tactician-api
"""

import sys
Expand Down Expand Up @@ -158,7 +158,7 @@ async def client_connected_cb(counter, args, reader, writer):

def my_parse_args():
parser = argparse.ArgumentParser(
description='example of python code interacting with coq-tactician-reinforce')
description='example of python code interacting with coq-tactician-api')

parser.add_argument('--interactive',
action='store_true',
Expand Down Expand Up @@ -190,7 +190,7 @@ def my_parse_args():


parser.add_argument('--tcp', action='store_true',
help='drive coq-tactician-reinforce with tcp/ip instead of stdin')
help='drive coq-tactician-api with tcp/ip instead of stdin')

parser.add_argument('--tcp-sessions',
type = int,
Expand All @@ -211,7 +211,7 @@ def my_parse_args():

parser.add_argument('--coqfile', type=str, default=None,
help=('path to coq source code file (.v extension) to execute'
'in coq-tactician-reinforce'
'in coq-tactician-api'
f'the default is {pytact.common.test_filename_stdin}'
f'for --tcp --with-coq default is {pytact.common.test_filename_tcp}'))

Expand Down
2 changes: 1 addition & 1 deletion pytact/tests/TestReinforceStdin.v
Original file line number Diff line number Diff line change
Expand Up @@ -2,4 +2,4 @@ Goal True -> True.
intro. apply H.
Qed.

Reinforce.
Tactician Explore.
2 changes: 1 addition & 1 deletion pytact/tests/TestReinforceTcp.v
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
Goal True -> True. intro. apply H. Qed.
Reinforce "127.0.0.1" 33333.
Tactician Explore "127.0.0.1" 33333.

6 changes: 3 additions & 3 deletions src/dune
Original file line number Diff line number Diff line change
@@ -1,15 +1,15 @@
(coq.pp (modules g_graph))
(library
(name tactician_reinforce_plugin)
(public_name coq-tactician-reinforce.plugin)
(name tactician_api_plugin)
(public_name coq-tactician-api.plugin)
(flags :standard -rectypes -w -27-53-55)
(modules (
"g_graph"
graph_extractor
graph_def
graph_visualizer
neural_learner
reinforce
explore
graph_generator_learner
graph_capnp_generator
graph_api
Expand Down
File renamed without changes.
6 changes: 3 additions & 3 deletions src/g_graph.mlg
Original file line number Diff line number Diff line change
Expand Up @@ -25,9 +25,9 @@ VERNAC COMMAND EXTEND LGraphProof CLASSIFIED AS QUERY STATE proof_query
| [ "Shared" "Graph" "Depth" int(d) "Proof" ] -> { fun ~pstate -> SimpleHashedViz.make_proof_graph ~def_depth:d pstate }
END

VERNAC COMMAND EXTEND Reinforce CLASSIFIED AS QUERY
| [ "Reinforce" ] -> { Reinforce.reinforce_stdin () }
| [ "Reinforce" string(ip_addr) int(port) ] -> { Reinforce.reinforce_tcp ip_addr port }
VERNAC COMMAND EXTEND Explore CLASSIFIED AS QUERY
| [ "Tactician" "Explore" ] -> { Explore.reinforce_stdin () }
| [ "Tactician" "Explore" string(ip_addr) int(port) ] -> { Explore.reinforce_tcp ip_addr port }
END

VERNAC COMMAND EXTEND CheckNeuralAlignment CLASSIFIED AS QUERY
Expand Down
1 change: 0 additions & 1 deletion tests/server_test0.v
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
(* Set Tactician Reinforce1 Debug. *)
Load NNLearner.
Set Tactician Neural Server "127.0.0.1:33333".
From Tactician Require Import Ltac1.
Expand Down
1 change: 0 additions & 1 deletion tests/server_test1.v
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
(* Set Tactician Reinforce1 Debug. *)
Load NNLearner.
Set Tactician Neural Server "127.0.0.1:33333".
From Tactician Require Import Ltac1.
Expand Down
1 change: 0 additions & 1 deletion tests/server_test3.v
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
(* Set Tactician Reinforce1 Debug. *)
Load NNLearner.
Set Tactician Neural Server "127.0.0.1:33333".
From Tactician Require Import Ltac1.
Expand Down
4 changes: 2 additions & 2 deletions theories/NNLearner.v
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
From Tactician Require Import Ltac1.Record.

Load TacticianReinforceDepLoader.
Load TacticianApiDepLoader.

Declare ML Module "tactician_reinforce_plugin".
Declare ML Module "tactician_api_plugin".
20 changes: 10 additions & 10 deletions theories/dune
Original file line number Diff line number Diff line change
@@ -1,16 +1,16 @@
(coq.theory
(name TacticianReinforce)
(package coq-tactician-reinforce)
(name TacticianApi)
(package coq-tactician-api)
(flags -q -noinit)
(modules )
(libraries
coq-tactician-reinforce.plugin
coq-tactician-api.plugin
))

(include_subdirs qualified)

(rule
(targets TacticianReinforceDepLoader.v injection-flags-dirs)
(targets TacticianApiDepLoader.v injection-flags-dirs)
(deps plugin_deps_generate_conf.ml ../src/dune )
(action (run ocaml -I %{lib:findlib:} str.cma findlib.cma
%{deps} %{targets})))
Expand All @@ -30,20 +30,20 @@
(run cat injection-flags-dirs injection-flags-loader))))

(install
(package coq-tactician-reinforce)
(files (NNLearner.v as coq/user-contrib/TacticianReinforce/NNLearner.v)
(TacticianReinforceDepLoader.v as coq/user-contrib/TacticianReinforce/TacticianReinforceDepLoader.v))
(package coq-tactician-api)
(files (NNLearner.v as coq/user-contrib/TacticianApi/NNLearner.v)
(TacticianApiDepLoader.v as coq/user-contrib/TacticianApi/TacticianApiDepLoader.v))
(section lib_root)
)

(install
(package coq-tactician-reinforce)
(package coq-tactician-api)
(files (../graph_api.capnp as graph_api.capnp))
(section share)
)


(install
(package coq-tactician-reinforce)
(package coq-tactician-api)
(section (site (coq-tactician plugins)))
(files (injection-flags as coq-tactician-reinforce/injection-flags)))
(files (injection-flags as coq-tactician-api/injection-flags)))
2 changes: 1 addition & 1 deletion theories/injection-flags-loader.in
Original file line number Diff line number Diff line change
@@ -1 +1 @@
-I %{coq:lib}%/user-contrib/TacticianReinforce -R %{coq:lib}%/user-contrib/TacticianReinforce TacticianReinforce -l NNLearner
-I %{coq:lib}%/user-contrib/TacticianApi -R %{coq:lib}%/user-contrib/TacticianApi TacticianApi -l NNLearner
2 changes: 1 addition & 1 deletion theories/plugin_deps_generate_conf.ml
Original file line number Diff line number Diff line change
Expand Up @@ -116,7 +116,7 @@ let extract_dune dune_filename =
let () =
if (Array.length Sys.argv) != 4 then (
debug_msg "usage: ocaml plugin_deps_generate_conf.ml dune \
TacticianReinforceDepLoader.v injection-flags ";
TacticianApiDepLoader.v injection-flags ";
exit 1)
else (
(* get libraries from dune, using watermark cut *)
Expand Down

0 comments on commit 4a88aca

Please sign in to comment.