axiom_selection_proof_status_spec.rb revision 6038b00107b7bc45a596b94529bfb544a3ed6a65
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsyncrequire 'spec_helper'
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsyncdescribe 'Axiom Selection: Proof Status', :http_interaction do
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync setup_hets
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync stub_fqdn_and_port_for_pipeline_generator
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync let(:generator) do
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync FixturesGeneration::PipelineGenerator.new
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync end
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync let(:user) { create :user }
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync let(:repository) { create :repository }
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync let(:ontology_fixture_file) { %w(prove/Simple_Implications casl) }
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync let(:ontology_filepath) { ontology_fixture_file.join('.') }
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync before { stub_hets_for(ontology_filepath) }
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync let(:parent_ontology_version) do
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync version = version_for_file(repository,
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync ontology_file(*ontology_fixture_file))
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync version.parse
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync version
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync end
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync let(:parent_ontology) { parent_ontology_version.ontology }
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync let(:ontology) do
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync parent_ontology.children.find_by_name('Group')
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync end
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync let(:theorem) { ontology.theorems.find_by_name('rightunit') }
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync let(:axioms) { ontology.axioms }
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync let(:prover) { create :prover }
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync let(:status_disproven) { create :proof_status_disproven }
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync let(:status_proven) { create :proof_status_proven }
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync context 'all axioms' do
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync let(:axiom_selection) { create :manual_axiom_selection, axioms: axioms }
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync let(:proof_attempt) do
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync create :proof_attempt, theorem: theorem, prover: prover
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync end
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync let!(:proof_attempt_configuration) do
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync pac = proof_attempt.proof_attempt_configuration
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync pac.axiom_selection = axiom_selection.axiom_selection
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync pac.prover = prover
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync pac
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync end
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync before do
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync generator.with_cassette(generate_cassette_name, :hets_prove_uri) do
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync ProofExecution.new(proof_attempt).call
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync end
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync end
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync it 'proven' do |example|
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync expect(proof_attempt.reload.proof_status).to eq(status_proven)
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync end
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync end
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync context 'no axioms (meaning all are used)' do
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync let(:axiom_selection) { create :manual_axiom_selection, axioms: [] }
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync let(:proof_attempt) do
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync create :proof_attempt, theorem: theorem, prover: prover
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync end
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync let!(:proof_attempt_configuration) do
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync pac = proof_attempt.proof_attempt_configuration
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync pac.axiom_selection = axiom_selection.axiom_selection
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync pac.prover = prover
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync pac
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync end
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync before do
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync generator.with_cassette(generate_cassette_name, :hets_prove_uri) do
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync ProofExecution.new(proof_attempt).call
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync end
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync end
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync it 'proven' do |example|
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync expect(proof_attempt.reload.proof_status).to eq(status_proven)
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync end
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync end
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync context 'not sufficient axioms' do
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync let(:axiom_selection) do
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync create :manual_axiom_selection, axioms: [axioms.first]
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync end
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync let(:proof_attempt) do
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync create :proof_attempt, theorem: theorem, prover: prover
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync end
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync let!(:proof_attempt_configuration) do
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync pac = proof_attempt.proof_attempt_configuration
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync pac.axiom_selection = axiom_selection.axiom_selection
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync pac.prover = prover
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync pac
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync end
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync before do
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync generator.with_cassette(generate_cassette_name, :hets_prove_uri) do
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync ProofExecution.new(proof_attempt).call
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync end
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync end
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync it 'disproven' do |example|
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync expect(proof_attempt.reload.proof_status).to eq(status_disproven)
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync end
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync end
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsyncend
b8e299dddd091ae24e0c08c45d91b8f937bd14d2vboxsync