1237 let the user select a prover #1263

eugenk · 2015-03-14T12:53:42Z

This shall fix #1237. This branch allows the user to select multiple available provers for proving. For each prover, a proof attempt is made. Those proof attempts are processed sequentially.

Possibly important notes

The prove/ route has been replaced by proofs/ to use the REST convention
The new ProofsController is completely rewritten and has nothing in common with the previous ProveController
I tried to make many small commits and to not revert previous changes in the same branch. It should be easier to review this pull request commit by commit.

This branch is based on the branch of #1262 (introduce_hets_options) instead of staging. It might be easier to review that one first.

tillmo · 2015-03-19T17:04:09Z

when trying to prove the goal in strict_partial_order with SPASS, I get NoMethodError: undefined method "prove" for #<Theorem:0x00000006b682e8>

eugenk · 2015-03-20T11:34:18Z

That's odd. Have you restarted the rails server after switching the branch to 1237-let_the_user_select_a_prover?

tillmo · 2015-03-20T12:33:28Z

yes. But I forgot to restart sidekiq - that solved the problem. Is there a simple way to do all these restarts with one command?

eugenk · 2015-03-20T12:35:54Z

Yes, you can stop invoker and start it again.
During development, we start everything with

invoker start invoker.ini

from the ontohub directory. Whenever we need to restart the web server and sidekiq, we simply hit Crtl+C and start invoker again.

tillmo · 2015-03-21T19:24:03Z

when I prove asymmetric in strict_partial_order with eprover, I get "Time taken -1 seconds". This is extremely fast...

tillmo · 2015-03-21T19:32:37Z

when I select several provers at once (i.e. for a CASL goal: leo, eprover, darwin, SPASS, Vampire, leoII,...), I get in the job queue:

 less than a minute from now    0   hets    CollectiveProofAttemptWorker    
"OntologyVersion", 28, [7, 8, 9, 10, 11, 12, 13, 18]   JSON::Stream::ParserError: Expected null keyword: char 1

If I select just one prover (SPASS), the theorem gets proven immediately.

eugenk · 2015-03-21T19:33:09Z

Yes, this seems to be a problem in hets, because it returns:

 "usedTime": {
  "seconds": -1,
  "components": { "hours": -1, "mins": 59, "secs": 59 }
  }

I can change ontohub to save 0 seconds if hets gives us a negative value.

tillmo · 2015-03-21T19:35:17Z

aha, the problem is not with selecting multiple provers, but with selecting leo. If leo is among the provers, the error occurs.

eugenk · 2015-03-21T19:42:25Z

That's too bad, I don't have leo on my machine. Could you please post the outputs of

curl -X GET http://localhost:8000/version
curl -X POST -d '{"format":"json","include":"true","prover":"leo","node":"strict_partial_order"}' -H 'Content-Type: application/json' http://localhost:8000/prove/http%3A%2F%2Flocalhost%3A3000%2Fref%2F1%2Fdefault%2Fpartial_order%2F%2Fstrict_partial_order/auto

This should attempt to prove strict_partial_order with leo.

tillmo · 2015-03-21T20:23:38Z

selecting QucikCheck leads to EOFError: end of file reached.
isabelle-process and isabelle-jedit lead to JSON::Stream::ParserError: Expected null keyword: char 1

tillmo · 2015-03-21T20:26:23Z

problem with leo solved. I has installed leo, but not ocaml. There should be a proper Ubuntu package for leo...

tillmo · 2015-03-21T20:32:58Z

the interactive Isabelle provers (with jedit, emacs etc.) should be removed from the list, because it is an own project to integrate them into Ontohub (see #136). I think Hets should provide some flag whether the prover is automatic or interactive.

tillmo · 2015-03-21T20:34:39Z

after selecting Isabellesledgehammer from the list of provers, I get a new prover in the list: Isabelle (sledgehammer), while Isabellesledgehammer remains in the list. Same with LeoII and Leo II.

tillmo · 2015-03-22T09:13:11Z

When I prove the goals in http://develop.ontohub.org/sandbox/Family2.het and select Pellet and Fact, I get a "THM", but the link links to a SPASS proof of a CASL theorem in strict_partial_order. Due to #1277, I could only reproduce this locally.

tillmo · 2015-03-22T09:28:36Z

in order to provide more details: here is the list of theorems that I have:

[2] pry(main)> Theorem.all
  Theorem Load (0.8ms)  SELECT "sentences".* FROM "sentences" WHERE "sentences"."imported" = 'f' AND "sentences"."type" IN ('Theorem')
=> [#<Theorem id: 1239, ontology_id: 5, name: "asymmetric", text: "forall x, y : elem . x < y => not y < x", range: "http://localhost:3000/ref/3/default/partial_order:1...", comments_count: 0, created_at: "2015-03-21 19:26:55", updated_at: "2015-03-21 20:52:30", display_text: "forall x, y : elem . x < y => not y < x", imported: false, type: "Theorem", proof_status_id: "THM", locid: "/default/partial_order//strict_partial_order//asymm...">,
 #<Theorem id: 1241, ontology_id: 6, name: "reflexive", text: "forall x : elem . x <= x", range: "http://localhost:3000/ref/3/default/partial_order:5...", comments_count: 0, created_at: "2015-03-21 19:26:55", updated_at: "2015-03-21 19:26:55", display_text: "forall x : elem . x <= x", imported: false, type: "Theorem", proof_status_id: "OPN", locid: "/default/partial_order//v__T//reflexive">,
 #<Theorem id: 1242, ontology_id: 6, name: "antisymmetric", text: "forall x, y : elem . x <= y /\\ y <= x => x = y", range: "http://localhost:3000/ref/3/default/partial_order:5...", comments_count: 0, created_at: "2015-03-21 19:26:55", updated_at: "2015-03-21 19:26:55", display_text: "forall x, y : elem . x <= y /\\ y <= x => x = y", imported: false, type: "Theorem", proof_status_id: "OPN", locid: "/default/partial_order//v__T//antisymmetric">,
 #<Theorem id: 1243, ontology_id: 6, name: "transitive", text: "forall x, y, z : elem . x <= y /\\ y <= z => x <= z", range: "http://localhost:3000/ref/3/default/partial_order:5...", comments_count: 0, created_at: "2015-03-21 19:26:55", updated_at: "2015-03-21 19:26:55", display_text: "forall x, y, z : elem . x <= y /\\ y <= z => x <= z", imported: false, type: "Theorem", proof_status_id: "OPN", locid: "/default/partial_order//v__T//transitive">,
 #<Theorem id: 1254, ontology_id: 21, name: "reflexive", text: "forall x : elem . x <= x", range: "http://localhost:3000/ref/1/default/partial_order2:...", comments_count: 0, created_at: "2015-03-21 19:28:29", updated_at: "2015-03-21 19:28:29", display_text: "forall x : elem . x <= x", imported: false, type: "Theorem", proof_status_id: "OPN", locid: "/default/partial_order2//v__T//reflexive">,
 #<Theorem id: 1255, ontology_id: 21, name: "antisymmetric", text: "forall x, y : elem . x <= y /\\ y <= x => x = y", range: "http://localhost:3000/ref/1/default/partial_order2:...", comments_count: 0, created_at: "2015-03-21 19:28:29", updated_at: "2015-03-21 19:28:29", display_text: "forall x, y : elem . x <= y /\\ y <= x => x = y", imported: false, type: "Theorem", proof_status_id: "OPN", locid: "/default/partial_order2//v__T//antisymmetric">,
 #<Theorem id: 1256, ontology_id: 21, name: "transitive", text: "forall x, y, z : elem . x <= y /\\ y <= z => x <= z", range: "http://localhost:3000/ref/1/default/partial_order2:...", comments_count: 0, created_at: "2015-03-21 19:28:29", updated_at: "2015-03-21 19:28:29", display_text: "forall x, y, z : elem . x <= y /\\ y <= z => x <= z", imported: false, type: "Theorem", proof_status_id: "OPN", locid: "/default/partial_order2//v__T//transitive">,
 #<Theorem id: 1252, ontology_id: 20, name: "asymmetric", text: "forall x, y : elem . x < y => not y < x", range: "http://localhost:3000/ref/1/default/partial_order2:...", comments_count: 0, created_at: "2015-03-21 19:28:29", updated_at: "2015-03-21 19:31:59", display_text: "forall x, y : elem . x < y => not y < x", imported: false, type: "Theorem", proof_status_id: "THM", locid: "/default/partial_order2//strict_partial_order//asym...">,
 #<Theorem id: 1277, ontology_id: 23, name: "Ax1_19", text: "Class: Mother\n       SubClassOf: Parent", range: "http://localhost:3000/ref/1/default/Family:56.10-56...", comments_count: 0, created_at: "2015-03-21 20:38:35", updated_at: "2015-03-22 08:54:08", display_text: "Class: Mother SubClassOf: Parent", imported: false, type: "Theorem", proof_status_id: "UNK", locid: "/default/Family//FamilyBase//Ax1_19">,
 #<Theorem id: 1278, ontology_id: 23, name: "Ax2_20", text: "Individual: mary\n            Types: Grandmother", range: "http://localhost:3000/ref/1/default/Family:57.16-57...", comments_count: 0, created_at: "2015-03-21 20:38:35", updated_at: "2015-03-22 08:54:12", display_text: "Individual: mary Types: Grandmother", imported: false, type: "Theorem", proof_status_id: "THM", locid: "/default/Family//FamilyBase//Ax2_20">,
 #<Theorem id: 1279, ontology_id: 23, name: "Ax3_21", text: "Class: Man\n       EquivalentTo: Woman", range: "http://localhost:3000/ref/1/default/Family:58.10-59...", comments_count: 0, created_at: "2015-03-21 20:38:35", updated_at: "2015-03-22 08:54:12", display_text: "Class: Man EquivalentTo: Woman", imported: false, type: "Theorem", proof_status_id: "NOC", locid: "/default/Family//FamilyBase//Ax3_21">]
[3] pry(main)>

Now, the link http://localhost:3000/repositories/default/ontologies/23/theorems/1278/proof_attempts/1 shows the correct ontology (FamilyBase), but "Proof attempt of asymmetric", where "asymmetric" is linked to http://localhost:3000/repositories/default/ontologies/23/theorems/1252, which actually does not exist, because it is a theorem id of strict_partial_order coupled with the ontology id of FamilyBase. It exists at http://localhost:3000/repositories/default/ontologies/20/theorems/1252/proof_attempts/1

tillmo · 2015-03-22T09:38:46Z

Actually, for all new theorems that I prove, when displaying the proof details with the proof_attempts URL, I always get the proof details of theorem 1252 (asymmetric).

eugenk · 2015-03-23T07:11:35Z

selecting QucikCheck leads to EOFError: end of file reached.
isabelle-process and isabelle-jedit lead to JSON::Stream::ParserError: Expected null keyword: char 1

I added #1280 for it.

the interactive Isabelle provers (with jedit, emacs etc.) should be removed from the list, because it is an own project to integrate them into Ontohub (see #136). I think Hets should provide some flag whether the prover is automatic or interactive.

I added #1281 for it.

after selecting Isabellesledgehammer from the list of provers, I get a new prover in the list: Isabelle (sledgehammer), while Isabellesledgehammer remains in the list. Same with LeoII and Leo II.

I don't understand this. Maybe you could show it in the meeting today?

Actually, for all new theorems that I prove, when displaying the proof details with the proof_attempts URL, I always get the proof details of theorem 1252 (asymmetric).

I'm working on it in the next branch (not pushed yet). There each ProofAttempt gets a locid and those are used for the links. Locally, this is working fine in the new branch.

This classes allow to (asynchronously) make many proof attempts sequentially. In a later phase, this will be reconstructed to work in parallel.

eugenk · 2015-03-26T05:39:09Z

This branch is now based on staging.

eugenk · 2015-03-26T12:43:37Z

jenkins, test this please

tillmo · 2015-03-28T07:16:58Z

app/controllers/proofs_controller.rb

+
+  def new
+    render template: 'proofs/new'
+  end


two new methods do not make sense

Fixed by 6a2fc9d

tillmo · 2015-03-31T08:16:47Z

👍

1237 let the user select a prover

coveralls · 2016-11-05T02:01:38Z

Changes Unknown when pulling 62aa918 on 1237-let_the_user_select_a_prover into * on staging*.

eugenk force-pushed the 1237-let_the_user_select_a_prover branch from bf4fd9a to 1a0ac07 Compare March 14, 2015 20:31

eugenk mentioned this pull request Mar 16, 2015

Union of provers lists #1265

Open

eugenk force-pushed the 1237-let_the_user_select_a_prover branch from 1a0ac07 to 635641b Compare March 18, 2015 15:10

tillmo mentioned this pull request Mar 20, 2015

Too many provers are shown spechub/Hets#1471

Closed

eugenk force-pushed the 1237-let_the_user_select_a_prover branch 4 times, most recently from 299ec76 to c159434 Compare March 25, 2015 05:43

eugenk mentioned this pull request Mar 25, 2015

1273 improve proving interface #1286

Merged

eugenk force-pushed the 1237-let_the_user_select_a_prover branch from c159434 to 9837c27 Compare March 25, 2015 07:55

eugenk assigned tillmo Mar 25, 2015

eugenk force-pushed the 1237-let_the_user_select_a_prover branch 2 times, most recently from 385121f to ae18542 Compare March 25, 2015 20:31

eugenk added 12 commits March 26, 2015 06:36

Add prover to ProveOptions.

295ab65

Pass ProveOptions to [async_]prove methods.

ca9cafc

Add CollectiveProofAttempt[Worker]

b26064e

This classes allow to (asynchronously) make many proof attempts sequentially. In a later phase, this will be reconstructed to work in parallel.

Add CollectiveProofAttempt spec.

0fa5567

Add CollectiveProofAttemptWorker spec.

3529534

Add Proof FakeRecord.

b44343a

Add Proof spec.

066e76b

Rename/substantivize ProveController and its route.

a69acbe

Rewrite ProofsController to use Proof FakeRecord.

7c409f3

Rewrite ProofsController spec.

e0ee22c

Add route, action and views for proofs#new.

543c1be

Always show prove button.

062415b

eugenk force-pushed the 1237-let_the_user_select_a_prover branch from ae18542 to 062415b Compare March 26, 2015 05:38

tillmo reviewed Mar 28, 2015
View reviewed changes

eugenk added 4 commits March 31, 2015 08:11

Remove duplicate new action.

6a2fc9d

Add comment on provers attribute.

940c9c3

Fix typos.

0af4266

Add comment on Proof class.

62aa918

eugenk added a commit that referenced this pull request Mar 31, 2015

Merge pull request #1263 from ontohub/1237-let_the_user_select_a_prover

5ac5ef3

1237 let the user select a prover

eugenk merged commit 5ac5ef3 into staging Mar 31, 2015

eugenk deleted the 1237-let_the_user_select_a_prover branch March 31, 2015 08:21

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

1237 let the user select a prover #1263

1237 let the user select a prover #1263

eugenk commented Mar 14, 2015

tillmo commented Mar 19, 2015

eugenk commented Mar 20, 2015

tillmo commented Mar 20, 2015

eugenk commented Mar 20, 2015

tillmo commented Mar 21, 2015

tillmo commented Mar 21, 2015

eugenk commented Mar 21, 2015

tillmo commented Mar 21, 2015

eugenk commented Mar 21, 2015

tillmo commented Mar 21, 2015

tillmo commented Mar 21, 2015

tillmo commented Mar 21, 2015

tillmo commented Mar 21, 2015

tillmo commented Mar 22, 2015

tillmo commented Mar 22, 2015

tillmo commented Mar 22, 2015

eugenk commented Mar 23, 2015

eugenk commented Mar 26, 2015

eugenk commented Mar 26, 2015

tillmo Mar 28, 2015

eugenk Mar 31, 2015

tillmo commented Mar 31, 2015

coveralls commented Nov 5, 2016

1237 let the user select a prover #1263

1237 let the user select a prover #1263

Conversation

eugenk commented Mar 14, 2015

Possibly important notes

tillmo commented Mar 19, 2015

eugenk commented Mar 20, 2015

tillmo commented Mar 20, 2015

eugenk commented Mar 20, 2015

tillmo commented Mar 21, 2015

tillmo commented Mar 21, 2015

eugenk commented Mar 21, 2015

tillmo commented Mar 21, 2015

eugenk commented Mar 21, 2015

tillmo commented Mar 21, 2015

tillmo commented Mar 21, 2015

tillmo commented Mar 21, 2015

tillmo commented Mar 21, 2015

tillmo commented Mar 22, 2015

tillmo commented Mar 22, 2015

tillmo commented Mar 22, 2015

eugenk commented Mar 23, 2015

eugenk commented Mar 26, 2015

eugenk commented Mar 26, 2015

tillmo Mar 28, 2015

Choose a reason for hiding this comment

eugenk Mar 31, 2015

Choose a reason for hiding this comment

tillmo commented Mar 31, 2015

coveralls commented Nov 5, 2016