Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update gems #1255

Merged
merged 54 commits into from
Jun 23, 2015
Merged

Update gems #1255

merged 54 commits into from
Jun 23, 2015

Conversation

eugenk
Copy link
Member

@eugenk eugenk commented Mar 11, 2015

This updates most gems to their current compatible version. I (mostly) created one commit per gem to make reverting/rebasing easier. If you want to, I will squash most of the commits before merging into staging. Please leave a comment on it.

I have not tested if 5a4e18f is okay. This depends on issue 1253 (see the commit message).

@0robustus1 0robustus1 self-assigned this May 4, 2015
@eugenk eugenk force-pushed the update_gems branch 2 times, most recently from b7eddb2 to 9c7fd4e Compare May 4, 2015 16:24
@eugenk
Copy link
Member Author

eugenk commented May 5, 2015

Why is Gemnasium inactive for ontohub? Dependency Status

@eugenk
Copy link
Member Author

eugenk commented May 5, 2015

I did one more round of gem updating. inherited_resources can't be just updated. It needs some error investigation. See #1340.

@0robustus1
Copy link
Contributor

Could you rebase/merge staging? On my system there are red-tests. I do not know if this is related.

@eugenk
Copy link
Member Author

eugenk commented May 27, 2015

Done

@ebolloff
Copy link
Member

When I run rake I get

Calling hets/prove on "spec/fixtures/ontologies/prove/Simple_Implications.casl"
rake aborted!
JSON::ParserError: 757: unexpected token at '*** Error: no matching translation or prover found
'

@eugenk
Copy link
Member Author

eugenk commented May 28, 2015

I can't reproduce this on my machine. Could you please delete the generated fixtures with

git clean -fdX spec/

and run rake again? Does the error still occur?

@0robustus1
Copy link
Contributor

Yep still occurs (at least one mine). Could we do a comparison of installed hets versions?

mine: version of hets: v0.99, 1430921534

@eugenk
Copy link
Member Author

eugenk commented May 28, 2015

I got the same version

@ebolloff
Copy link
Member

I still get the error on this branch. My hets version version of hets: v0.99, 1431506945.

@eugenk
Copy link
Member Author

eugenk commented May 29, 2015

Given that your hets server runs, what does this command print?

curl -X POST -H "Content-Type: application/json" -d '{"format":"json"}' http://localhost:8000/prove/file%3A%2F%2F%2Fescaped%2Fpath%2Fto%2Fontohub%2Fspec%2Ffixtures%2Fontologies%2Fprove%2FSimple_Implications.casl/auto

(Note that you need to adjust the escaped path)

@0robustus1
Copy link
Contributor

[{
"node": "CounterSatisfiable",
"goals": [{
 "name": "Ax2",
 "result": "Disproved",
 "details": "",
 "used_prover": { "identifier": "SPASS", "name": "SPASS" },
 "used_translation": "CASL2SoftFOL",
 "tactic_script": {
  "time_limit": 1, "extra_options": [ "-DocProof"] },
 "proof_tree": "",
 "used_time": {
  "seconds": 0, "components": { "hours": 0, "mins": 0, "secs": 0 }
  },
 "used_axioms": [],
 "prover_output":
  "\n--------------------------SPASS-START-----------------------------\nInput Problem:\n1[0:Inp] ||  -> equal(zero,one)**.\n2[0:Inp] ||  -> equal(U,zero)*.\n This is a unit equality problem.\n This is a problem that has, if any, a finite domain model.\n There is a finite domain clause.\n There are no function symbols.\n The conjecture is ground.\n Axiom clauses: 1 Conjecture clauses: 1\n Inferences: ISpR=1 ISpL=1 \n Reductions: RFRew=1 RBRew=1 RFMRR=1 RBMRR=1 RObv=1 RUnC=1 RTaut=1 RFSub=1 RBSub=1 \n Extras    : Input Saturation, Always Selection, No Splitting, Full Reduction,  Ratio: 5, FuncWeight: 1, VarWeight: 1\n Precedence: zero > one\n Ordering  : KBO\nProcessed Problem:\n\nWorked Off Clauses:\n\nUsable Clauses:\n3[0:Rew:1.0,2.0] ||  -> equal(U,one)*.\n\tGiven clause: 3[0:Rew:1.0,2.0] ||  -> equal(U,one)*.\n\tGiven clause: 5[0:SpR:3.0,3.0] ||  -> equal(U,V)*.\nSPASS V 3.7 \nSPASS beiseite: Completion found.\nProblem: Read from stdin. \nSPASS derived 3 clauses, backtracked 0 clauses, performed 0 splits and kept 4 clauses.\nSPASS allocated 45932 KBytes.\nSPASS spent\t0:00:00.03 on the problem.\n\t\t0:00:00.01 for the input.\n\t\t0:00:00.01 for the FLOTTER CNF translation.\n\t\t0:00:00.00 for inferences.\n\t\t0:00:00.00 for the backtracking.\n\t\t0:00:00.00 for the reduction.\n\n\n The saturated set of worked-off clauses is :\n5[0:SpR:3.0,3.0] ||  -> equal(U,V)*.\n--------------------------SPASS-STOP------------------------------\n"
 }]
}, {
"node": "Theorem",
"goals": [{
 "name": "Ax1",
 "result": "Proved",
 "details": "",
 "used_prover": { "identifier": "SPASS", "name": "SPASS" },
 "used_translation": "CASL2SoftFOL",
 "tactic_script": {
  "time_limit": 1, "extra_options": [ "-DocProof"] },
 "proof_tree": "",
 "used_time": {
  "seconds": 0, "components": { "hours": 0, "mins": 0, "secs": 0 }
  },
 "used_axioms": [],
 "prover_output":
  "\n--------------------------SPASS-START-----------------------------\nInput Problem:\n1[0:Inp] || equal(skc1,skc1)* -> .\n This is a unit equality problem.\n This is a problem that has, if any, a finite domain model.\n There are no function symbols.\n The conjecture is ground.\n Axiom clauses: 0 Conjecture clauses: 1\n Inferences: IEqR=1 \n Reductions: RFMRR=1 RBMRR=1 RObv=1 RUnC=1 RTaut=1 RFSub=1 RBSub=1 \n Extras    : Input Saturation, Always Selection, No Splitting, Full Reduction,  Ratio: 5, FuncWeight: 1, VarWeight: 1\n Precedence: zero > skc0 > skc1\n Ordering  : KBO\nProcessed Problem:\n\nWorked Off Clauses:\n\nUsable Clauses:\n\nSPASS V 3.7 \nSPASS beiseite: Proof found.\nProblem: Read from stdin. \nSPASS derived 0 clauses, backtracked 0 clauses, performed 0 splits and kept 1 clauses.\nSPASS allocated 45930 KBytes.\nSPASS spent\t0:00:00.03 on the problem.\n\t\t0:00:00.01 for the input.\n\t\t0:00:00.01 for the FLOTTER CNF translation.\n\t\t0:00:00.00 for inferences.\n\t\t0:00:00.00 for the backtracking.\n\t\t0:00:00.00 for the reduction.\n\n\nHere is a proof with depth 0, length 2 :\n1[0:Inp] || equal(skc1,skc1)* -> .\n2[0:Obv:1.0] ||  -> .\nFormulae used in the proof : ax1\n\n--------------------------SPASS-STOP------------------------------\n"
 }]
}, {
"node": "Group",
"goals": [{
 "name": "rightunit",
 "result": "Proved",
 "details": "",
 "used_prover": { "identifier": "SPASS", "name": "SPASS" },
 "used_translation": "CASL2SoftFOL",
 "tactic_script": {
  "time_limit": 1, "extra_options": [ "-DocProof"] },
 "proof_tree": "",
 "used_time": {
  "seconds": 0, "components": { "hours": 0, "mins": 0, "secs": 0 }
  },
 "used_axioms": [ "leftunit", "Ax2", "ga_assoc___+__"],
 "prover_output":
  "\n--------------------------SPASS-START-----------------------------\nInput Problem:\n1[0:Inp] ||  -> equal(o__Plus__(U,zero),U)**.\n2[0:Inp] || equal(o__Plus__(zero,skc1),skc1)** -> .\n3[0:Inp] ||  -> equal(o__Plus__(U,minus__(U)),zero)**.\n4[0:Inp] ||  -> equal(o__Plus__(o__Plus__(U,V),W),o__Plus__(U,o__Plus__(V,W)))**.\n This is a unit equality problem.\n This is a problem that has, if any, a non-trivial domain model.\n The conjecture is ground.\n Axiom clauses: 3 Conjecture clauses: 1\n Inferences: IEqR=1 ISpR=1 ISpL=1 \n Reductions: RFRew=1 RBRew=1 RFMRR=1 RBMRR=1 RObv=1 RUnC=1 RTaut=1 RFSub=1 RBSub=1 \n Extras    : Input Saturation, No Selection, No Splitting, Full Reduction,  Ratio: 5, FuncWeight: 1, VarWeight: 1\n Precedence: o__Plus__ > minus__ > skc1 > skc0 > zero\n Ordering  : KBO\nProcessed Problem:\n\nWorked Off Clauses:\n\nUsable Clauses:\n1[0:Inp] ||  -> equal(o__Plus__(U,zero),U)**.\n2[0:Inp] || equal(o__Plus__(zero,skc1),skc1)** -> .\n3[0:Inp] ||  -> equal(o__Plus__(U,minus__(U)),zero)**.\n4[0:Inp] ||  -> equal(o__Plus__(o__Plus__(U,V),W),o__Plus__(U,o__Plus__(V,W)))**.\n\tGiven clause: 1[0:Inp] ||  -> equal(o__Plus__(U,zero),U)**.\n\tGiven clause: 2[0:Inp] || equal(o__Plus__(zero,skc1),skc1)** -> .\n\tGiven clause: 3[0:Inp] ||  -> equal(o__Plus__(U,minus__(U)),zero)**.\n\tGiven clause: 4[0:Inp] ||  -> equal(o__Plus__(o__Plus__(U,V),W),o__Plus__(U,o__Plus__(V,W)))**.\n\tGiven clause: 11[0:SpR:1.0,4.0] ||  -> equal(o__Plus__(U,o__Plus__(zero,V)),o__Plus__(U,V))**.\n\tGiven clause: 21[0:Rew:1.0,20.0] ||  -> equal(o__Plus__(U,minus__(zero)),U)**.\n\tGiven clause: 8[0:SpR:4.0,3.0] ||  -> equal(o__Plus__(U,o__Plus__(V,minus__(o__Plus__(U,V)))),zero)**.\n\tGiven clause: 12[0:SpR:3.0,4.0] ||  -> equal(o__Plus__(U,o__Plus__(minus__(U),V)),o__Plus__(zero,V))**.\n\tGiven clause: 67[0:Rew:1.0,61.0] ||  -> equal(o__Plus__(zero,minus__(minus__(U))),U)**.\nSPASS V 3.7 \nSPASS beiseite: Proof found.\nProblem: Read from stdin. \nSPASS derived 48 clauses, backtracked 0 clauses, performed 0 splits and kept 17 clauses.\nSPASS allocated 46026 KBytes.\nSPASS spent\t0:00:00.14 on the problem.\n\t\t0:00:00.08 for the input.\n\t\t0:00:00.05 for the FLOTTER CNF translation.\n\t\t0:00:00.00 for inferences.\n\t\t0:00:00.00 for the backtracking.\n\t\t0:00:00.00 for the reduction.\n\n\nHere is a proof with depth 3, length 11 :\n1[0:Inp] ||  -> equal(o__Plus__(U,zero),U)**.\n2[0:Inp] || equal(o__Plus__(zero,skc1),skc1)** -> .\n3[0:Inp] ||  -> equal(o__Plus__(U,minus__(U)),zero)**.\n4[0:Inp] ||  -> equal(o__Plus__(o__Plus__(U,V),W),o__Plus__(U,o__Plus__(V,W)))**.\n11[0:SpR:1.0,4.0] ||  -> equal(o__Plus__(U,o__Plus__(zero,V)),o__Plus__(U,V))**.\n12[0:SpR:3.0,4.0] ||  -> equal(o__Plus__(U,o__Plus__(minus__(U),V)),o__Plus__(zero,V))**.\n61[0:SpR:3.0,12.0] ||  -> equal(o__Plus__(zero,minus__(minus__(U))),o__Plus__(U,zero))**.\n67[0:Rew:1.0,61.0] ||  -> equal(o__Plus__(zero,minus__(minus__(U))),U)**.\n77[0:SpR:67.0,11.0] ||  -> equal(o__Plus__(U,minus__(minus__(V))),o__Plus__(U,V))**.\n79[0:Rew:77.0,67.0] ||  -> equal(o__Plus__(zero,U),U)**.\n80[0:UnC:79.0,2.0] ||  -> .\nFormulae used in the proof : leftunit rightunit ax2 ga_assoc___Plus__\n\n--------------------------SPASS-STOP------------------------------\n"
 }, {
 "name": "zero_plus",
 "result": "Proved",
 "details": "",
 "used_prover": { "identifier": "SPASS", "name": "SPASS" },
 "used_translation": "CASL2SoftFOL",
 "tactic_script": {
  "time_limit": 1, "extra_options": [ "-DocProof"] },
 "proof_tree": "",
 "used_time": {
  "seconds": 0, "components": { "hours": 0, "mins": 0, "secs": 0 }
  },
 "used_axioms": [ "rightunit"],
 "prover_output":
  "\n--------------------------SPASS-START-----------------------------\nInput Problem:\n1[0:Inp] ||  -> equal(o__Plus__(zero,U),U)**.\n2[0:Inp] ||  -> equal(o__Plus__(U,zero),U)**.\n3[0:Inp] || equal(o__Plus__(zero,zero),zero)** -> .\n4[0:Inp] ||  -> equal(o__Plus__(U,minus__(U)),zero)**.\n5[0:Inp] ||  -> equal(o__Plus__(o__Plus__(U,V),W),o__Plus__(U,o__Plus__(V,W)))**.\n This is a unit equality problem.\n This is a problem that has, if any, a non-trivial domain model.\n The conjecture is ground.\n Axiom clauses: 4 Conjecture clauses: 1\n Inferences: IEqR=1 ISpR=1 ISpL=1 \n Reductions: RFRew=1 RBRew=1 RFMRR=1 RBMRR=1 RObv=1 RUnC=1 RTaut=1 RFSub=1 RBSub=1 \n Extras    : Input Saturation, No Selection, No Splitting, Full Reduction,  Ratio: 5, FuncWeight: 1, VarWeight: 1\n Precedence: o__Plus__ > minus__ > zero\n Ordering  : KBO\nProcessed Problem:\n\nWorked Off Clauses:\n\nUsable Clauses:\n1[0:Inp] ||  -> equal(o__Plus__(zero,U),U)**.\n2[0:Inp] ||  -> equal(o__Plus__(U,zero),U)**.\n4[0:Inp] ||  -> equal(o__Plus__(U,minus__(U)),zero)**.\n5[0:Inp] ||  -> equal(o__Plus__(o__Plus__(U,V),W),o__Plus__(U,o__Plus__(V,W)))**.\nSPASS V 3.7 \nSPASS beiseite: Proof found.\nProblem: Read from stdin. \nSPASS derived 0 clauses, backtracked 0 clauses, performed 0 splits and kept 4 clauses.\nSPASS allocated 45941 KBytes.\nSPASS spent\t0:00:00.05 on the problem.\n\t\t0:00:00.01 for the input.\n\t\t0:00:00.02 for the FLOTTER CNF translation.\n\t\t0:00:00.00 for inferences.\n\t\t0:00:00.00 for the backtracking.\n\t\t0:00:00.00 for the reduction.\n\n\nHere is a proof with depth 0, length 4 :\n1[0:Inp] ||  -> equal(o__Plus__(zero,U),U)**.\n3[0:Inp] || equal(o__Plus__(zero,zero),zero)** -> .\n6[0:Rew:1.0,3.0] || equal(zero,zero)* -> .\n7[0:Obv:6.0] ||  -> .\nFormulae used in the proof : rightunit zero_plus\n\n--------------------------SPASS-STOP------------------------------\n"
 }]
}]

@ebolloff
Copy link
Member

👍

eugenk added a commit that referenced this pull request Jun 23, 2015
@eugenk eugenk merged commit 1a5800e into staging Jun 23, 2015
@eugenk eugenk deleted the update_gems branch June 23, 2015 04:18
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

4 participants