brando90 isabelle-gym issues

brando90 / isabelle-gym

MIT License

2 stars 0 forks source link

issues

Newest

Newest Most commented Recently updated Oldest Least commented Least recently updated

advertise on zulip

#35 brando90 opened 3 years ago
0
Create LICENSE

#34 brando90 closed 3 years ago
0
Isagym.isar + Sketching agent

#32 brando90 closed 3 years ago
0
Tactician agent for IsaGym

#31 brando90 opened 3 years ago
0
Make datasets.

#30 madun1999 opened 4 years ago
3
Establish grammar for tactics used in isabelle gym.

#29 brando90 closed 4 years ago
2
Have our parser be complete and not lose information of HOL terms

#28 brando90 closed 3 years ago
0
Short cut API for gym

#27 brando90 closed 3 years ago
0
Benchmarking Single Theorem Document vs other RL Gyms & HOList

#26 brando90 closed 3 years ago
0
Extract entities/structure from HOL terms (for the agent)

#25 brando90 closed 4 years ago
1
Understand how (and why) the external sources can help (e.g. isabelle dev team, vscode plugin dev team)

#24 brando90 closed 4 years ago
0
I will brainstorm on how to contact the Isabelle team

#23 brando90 closed 4 years ago
0
How does the Multi-threading affect our python client?

#22 brando90 closed 3 years ago
0
Send the initial lemma to Isabelle and get it back in python (if done send next line, apply)

#21 brando90 closed 4 years ago
1
Docker image for Isabelle-Gym

#20 brando90 opened 4 years ago
0
Collect a Data set of proofs for Iabelle-Gym

#19 brando90 closed 3 years ago
0
Push Brando's Isar code

#18 brando90 closed 4 years ago
0
Make sure Isar works with our protocol, write a test for Isar (through our python API)

#17 brando90 closed 4 years ago
1
Everyone learn Scala

#16 brando90 closed 4 years ago
0
Have a pseudo API for HOList & CoqGym to compare to our API

#15 brando90 closed 4 years ago
1
Availability of using sledgehammer

#14 brando90 closed 4 years ago
0
Apply a tactic and get the AST goals for the agent in python

#13 brando90 closed 3 years ago
2
Having the current facts for the agent available in Python

#12 brando90 opened 4 years ago
4
BRANDO: give feedback joint answer:

#11 brando90 closed 3 years ago
0
Draw project structure.

#10 jizej closed 3 years ago
0
write a prototype API in a google doc that imitates HOList

#9 brando90 closed 4 years ago
0
Write a demo that communicates with Isabelle server in python through text exchanges and complete some simple lemmas using auto according to the protype API based on HOList.

#8 brando90 closed 4 years ago
0
edited joint group answer with Brando

#7 brando90 closed 3 years ago
1
joint group answer

#6 brando90 closed 4 years ago
1
individual answers

#5 brando90 closed 4 years ago
0
RL agent proposal for Isabelle-Gym

#4 brando90 opened 4 years ago
0
Data set of proofs in Isabelle

#3 brando90 closed 3 years ago
0
Design first Isabelle pseudo API

#2 brando90 opened 4 years ago
6
Literature Review if Isabelle Gym already exists

#1 brando90 closed 4 years ago
10