1284 show theorem and proof attempt state #1312
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
eugenk
force-pushed
the
1284-show_theorem_and_proof_attempt_state
branch
from
4ea99c7
to
85d4852
Compare
eugenk
force-pushed
the
1284-show_theorem_and_proof_attempt_state
branch
6 times, most recently
from
1268e62
to
be139c0
Compare
eugenk
force-pushed
the
1284-show_theorem_and_proof_attempt_state
branch
3 times, most recently
from
ccfd9f7
to
21ca583
Compare
|
I rebased this on staging. |
|
when trying this with legacy data, I get an error in Details at https://gist.github.com/tillmo/7a3bcb2b74c96fbc718b |
|
That's odd. I can't find any occurrence of |
|
I can't reproduce this error using data that I created on staging.ontohub.org. This branch is a little older than staging. Could you open the rails console and execute the following, please: Theorem.find_with_locid('/test/Family//FamilyBase//Ax1_19').proof_attempts.each { |pa| puts pa.inspect; puts }What is being printed to the console? |
|
sorry, that line was the botton of the stack trace. The top is |
|
Here is the console output: |
|
Please run |
|
I get |
|
Alright. It seems like I need to redo the data migrations rather sooner than later. |
|
maybe the problem has been caused by the fact that I was not disciplined enough to run the data migrations each time, and therefore db and data migrations have been exectued in wrong order? |
|
Even if that caused the problem, this should not happen. I'm fixing the data migrations right now. |
|
#1335 should fix the migration problem. |
|
OK, my problem has been solved by #1335 (although it still occurs here, but I assume that I can safely ignore that). |
| @@ -13,9 +13,6 @@ class OntologiesController < InheritedResources::Base | |||
|
|
|||
| respond_to :html, except: %i(show) | |||
|
|
|||
| before_filter :check_write_permission, except: [:index, :show, :oops_state] | |||
| before_filter :check_read_permissions | |||
There was a problem hiding this comment.
why are these before_filters removed?
There was a problem hiding this comment.
This is odd. It should not have happened. I probably messed something up with my editor without noticing it. This change is removed (by commit amend) in 318de55.
eugenk
force-pushed
the
1284-show_theorem_and_proof_attempt_state
branch
from
21ca583
to
41543d0
Compare
|
I just rebased this on staging and amended the odd commit removing the before filters. |
Now we are consistent with the theorems index view.
eugenk
force-pushed
the
1284-show_theorem_and_proof_attempt_state
branch
from
41543d0
to
f4e0204
Compare
|
Rebased again. I made a mistake in the last rebase. The amended commit is now 06cbff1. |
|
👍 |
eugenk
added a commit
that referenced
this pull request
May 4, 2015
…empt_state 1284 show theorem and proof attempt state
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This shall fix #1284. It also adds retry functionality to failed proof attempts.
The branch of this pull request is based on:add_tactic_script_model (Add tactic script model #1311)1256-add_proving_related_serializers (1256 add proving related serializers #1289)The first commit of this branch is:Move state helper to own module and generalize it. 33f017c