ml4tp / gamepad Goto Github PK
View Code? Open in Web Editor NEWA Learning Environment for Theorem Proving
License: Apache License 2.0
A Learning Environment for Theorem Proving
License: Apache License 2.0
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')
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.
Is there documentation/API?
Which is incoherent with the last instructions of the README?
paper says they are a function of the tactic predictor, but no details of what that means are provided.
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?
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
instructions say:
Check that you are using tcoq.
which coqc
what do we want to see to know tcoq is being used?
after installing ocamlfind
need to run the following to update path in my setting.
eval $(opam config env)
FYI
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']
)
./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
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?
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.