ml4tp / gamepad Goto Github PK

View Code? Open in Web Editor NEW

67.0 67.0 15.0 55.09 MB

A Learning Environment for Theorem Proving

License: Apache License 2.0

Shell 0.18% Python 48.16% Coq 48.97% Jupyter Notebook 2.69%

coq machine-learning python theorem-proving

gamepad's People

Contributors

Stargazers

Watchers

Forkers

nunofernandes-plight brando90 kappa666 takuyahiraoka zygi csaroff cbmm xujiesi liby99 wjsxlb2017 rowhit chrisbender sailfish009 muflhi01 fundou

gamepad's Issues

What is the API for position evaluation and how was it used?

build tcoq failed.

./build_tcoq.sh failed with the following error message. give me some hint pls.

neil@neil-System-Product-Name:~/Projects/gamepad$ sudo ./build_tcoq.sh 
~/Projects/gamepad/tcoq ~/Projects/gamepad
...
make --warn-undefined-variable --no-builtin-rules -f Makefile.build install
make[1]: Entering directory '/home/neil/Projects/gamepad/tcoq'
install -d "build/bin"
# recopie des fichiers de style pour coqide
install -d "build/lib/coq"/tools/coqdoc
touch "build/lib/coq"/tools/coqdoc/coqdoc.sty "build/lib/coq"/tools/coqdoc/coqdoc.css # to have the mode according to umask (bug #1715)
install -m 644  tools/coqdoc/coqdoc.css tools/coqdoc/coqdoc.sty "build/lib/coq"/tools/coqdoc
install bin/coqdep bin/coq_makefile bin/gallina bin/coq-tex bin/coqwc bin/coqdoc bin/coqc bin/coqworkmgr "build/bin"
install -d "build/bin"
install bin/coqc bin/coqtop.byte bin/coqtop bin/coqchk "build/bin"
Makefile.install:66: recipe for target 'install-binaries' failed
make[1]: Leaving directory '/home/neil/Projects/gamepad/tcoq'
Makefile:154: recipe for target 'submake' failed
~/Projects/gamepad
neil@neil-System-Produc

suggestion: Use eval to add path in zsh+iTerminal

after installing ocamlfind
need to run the following to update path in my setting.

eval $(opam config env)

FYI

including a setup.py for depedencies

it would be nice to include a dependencies file for depedencies, e.g.

from setuptools import setup

setup(
name='my_tf_proj', #project name
version='0.1.0',
description='my research library for deep learning',
#url
author='Me',
author_email='[email protected]',
license='MIT',
packages=['my_tf_pkg','cifar10','sgd_lib'],
#install_requires=['numpy','keras','namespaces','pdb','scikit-learn','scipy','virtualenv']
#install_requires=['numpy','keras','namespaces','pdb']
install_requires=['numpy','namespaces','pdb','scikit-learn','scipy','maps','pandas','matplotlib']
)

issues installing

the instructions are a bit unclear. I real ./get_data.sh then I did ./setup_tcoq.sh but I get error:

./setup_tcoq.sh
~/home_simulation_research/gamepad/tcoq ~/home_simulation_research/gamepad
Configuring Coq...
make: *** No rule to make target `clean'.  Stop.
mkdir: build: File exists
./setup_tcoq.sh: line 7: ./configure: No such file or directory
~/home_simulation_research/gamepad

what is configure and how do we get it?

How do I make sure I am using TCOQ

instructions say:

Check that you are using tcoq.
which coqc
what do we want to see to know tcoq is being used?

Where are the position evaluation models?

paper says they are a function of the tactic predictor, but no details of what that means are provided.

Error when trying to create `tacst.pickle` file via tacst_prep.py

I'm trying to create for one of the foo files. But there are errors, namely ZeroDivisionError for foo1, foo4, foo5, foo6 and foo8, and NameError for the other foo files from ~/examples. What is happening here?

Here is my output for each type of error:

(gamepad_venv)$ coqc examples/foo4.v > examples/foo.dump; python3 gamepad/tactr_prep.py file foo.dump -p examples;  python3 gamepad/ml/tacst_prep.py
==================================================
Reconstructing file examples/foo.dump
progress: 0.50% @ foo4
Loading tactr.pickle...
Creating dataset tactr.pickle...
Working on (0/1) foo4
tacsts 3 avg_size 11.0 avg_mid_size 11.0 avg_mid_noimp_size 11.0
TACTICS {'<coretactics::split@0>', '<coretactics::assumption@0>', '<coretactics::intro@0>', '<g_auto::auto@0> $n $lems $db'}
TACHIST
TAC <coretactics::intro@0> 2
TAC ml4tp.MYDONE 0
TAC <coretactics::clear@0> 0
TAC <coretactics::exact@0> 0
TAC <coretactics::constructor@0> 0
TAC <coretactics::left@0> 0
TAC <coretactics::right@0> 0
TAC <coretactics::split@0> 0
TAC <coretactics::symmetry@0> 0
TAC <coretactics::transitivity@0> 0
TAC <g_auto::auto@0> 1
TAC apply 0
TAC case 0
TAC compute 0
TAC <ssreflect_plugin::ssrcongr@0> 0
TAC <ssreflect_plugin::ssrelim@0> 0
TAC <ssreflect_plugin::ssrhave@0> 0
TAC <ssreflect_plugin::ssrmove@0> 0
TAC <ssreflect_plugin::ssrpose@0> 0
TAC <ssreflect_plugin::ssrrewrite@0> 0
TAC <ssreflect_plugin::ssrset@0> 0
TAC <ssreflect_plugin::ssrsuff@0> 0
TAC <ssreflect_plugin::ssrtcldo@0> 0
TAC <ssreflect_plugin::ssrwithoutloss@0> 0
Split Train=1 Valid=0 Test=0
Split Tactrs Train=3 Valid=0 Test=0
Traceback (most recent call last):
  File "gamepad/ml/tacst_prep.py", line 350, in <module>
    tacst_dataset = tacst.split_by_lemma()
  File "gamepad/ml/tacst_prep.py", line 312, in split_by_lemma
    ps = [len(data_train) / len(train), len(data_val) / len(val), len(data_test) / len(test)]
ZeroDivisionError: division by zero

(gamepad_venv)$ coqc examples/foo3.v > examples/foo.dump; python3 gamepad/tactr_prep.py file foo.dump -p examples;  python3 gamepad/ml/tacst_prep.py
==================================================
Reconstructing file examples/foo.dump
progress: 0.17% @ foo2
Loading tactr.pickle...
Creating dataset tactr.pickle...
Working on (0/1) foo2
Traceback (most recent call last):
  File "gamepad/ml/tacst_prep.py", line 350, in <module>
    tacst_dataset = tacst.split_by_lemma()
  File "gamepad/ml/tacst_prep.py", line 286, in split_by_lemma
    self.mk_tactrs()
  File "gamepad/ml/tacst_prep.py", line 227, in mk_tactrs
    self.mk_tactr(tactr_id, tactr)
  File "gamepad/ml/tacst_prep.py", line 273, in mk_tactr
    tac_bin = self.tac_bin(tac)
  File "gamepad/ml/tacst_prep.py", line 239, in tac_bin
    raise NameError("Not assigned to bin", tac[-1].name)
NameError: ('Not assigned to bin', 'induction n')

build tcoq failed

OK, my error, the OCaml was not probably set to version 4.05.0, it was set to an old one.

maybe others have the same problem, so I keep the description:

I get the following error running ./build_tcoq.sh

Makefile.install:66: die Regel für Ziel „install-binaries“ scheiterte
make[1]: Verzeichnis „/home/detlef/RNN/gamepad/tcoq“ wird verlassen
Makefile:154: die Regel für Ziel „submake“ scheiterte

in tcoq/build.log:
Makefile.build:542: die Regel für Ziel „printing/ptcoq.cmo“ scheiterte
make[1]: Verzeichnis „/home/detlef/RNN/gamepad/tcoq“ wird verlassen
Makefile:154: die Regel für Ziel „submake“ scheiterte

if I run make in the tcoq subdir I get more detailed info:
File "printing/ptcoq.ml", line 46, characters 8-22:
Error: Unbound value Sys.getenv_opt
Makefile.build:542: die Regel für Ziel „printing/ptcoq.cmo“ scheiterte
make[1]: *** [printing/ptcoq.cmo] Fehler 2
make[1]: Verzeichnis „/home/detlef/RNN/gamepad/tcoq“ wird verlassen
Makefile:154: die Regel für Ziel „submake“ scheiterte
make: *** [submake] Fehler 2

I tried to carefully follow the instructions, any hints would be great, thanks

Failed to Build tcoq

Hello,
I'm building toq on macOS and I saw this error in my tcoq/time.log when executing build_tcoq.sh:

*** Warning: in file theories/Init/Notations.v, declared ML module coretactics has not been found!
*** Warning: in file theories/Init/Notations.v, declared ML module extratactics has not been found!
*** Warning: in file theories/Init/Notations.v, declared ML module g_auto has not been found!
*** Warning: in file theories/Init/Notations.v, declared ML module g_class has not been found!
*** Warning: in file theories/Init/Notations.v, declared ML module g_eqdecide has not been found!
*** Warning: in file theories/Init/Notations.v, declared ML module g_rewrite has not been found!
*** Warning: in file theories/Init/Notations.v, declared ML module coretactics has not been found!
*** Warning: in file theories/Init/Notations.v, declared ML module extratactics has not been found!
*** Warning: in file theories/Init/Notations.v, declared ML module g_auto has not been found!
*** Warning: in file theories/Init/Notations.v, declared ML module g_class has not been found!
*** Warning: in file theories/Init/Notations.v, declared ML module g_eqdecide has not been found!
*** Warning: in file theories/Init/Notations.v, declared ML module g_rewrite has not been found!
File "lib/pp_control.ml", line 61, characters 22-33:
Error: This expression has type bytes -> int -> int -> unit
       but an expression was expected of type string -> int -> int -> unit
       Type bytes is not compatible with type string 
make[1]: *** [lib/pp_control.cmo] Error 2
make[1]: *** Waiting for unfinished jobs....
make: *** [submake] Error 2
install: bin/coqdep: No such file or directory
make[1]: *** [install-tools] Error 71
make: *** [submake] Error 2

real	1m4.070s
user	0m54.648s
sys	0m58.573s

Any idea? Thanks.

make file missing?

I asked:

then googled error (https://stackoverflow.com/questions/4182118/make-clean-results-in-no-rule-to-make-target-clean):

make: *** No rule to make target `clean'.  Stop.

and it seems a makefile is missing. Anyone mind pushing the right one?

No setup.py to install the gamepad module

Which is incoherent with the last instructions of the README?