{"action":"created","issue":{"url":"https://api.github.com/repos/jonsterling/JonPRL/issues/113","labels_url":"https://api.github.com/repos/jonsterling/JonPRL/issues/113/labels{/name}","comments_url":"https://api.github.com/repos/jonsterling/JonPRL/issues/113/comments","events_url":"https://api.github.com/repos/jonsterling/JonPRL/issues/113/events","html_url":"https://github.com/jonsterling/JonPRL/pull/113","id":92470349,"number":113,"title":"Add lazy theorem proving","user":{"login":"jozefg","id":814961,"avatar_url":"https://avatars.githubusercontent.com/u/814961?v=3","gravatar_id":"","url":"https://api.github.com/users/jozefg","html_url":"https://github.com/jozefg","followers_url":"https://api.github.com/users/jozefg/followers","following_url":"https://api.github.com/users/jozefg/following{/other_user}","gists_url":"https://api.github.com/users/jozefg/gists{/gist_id}","starred_url":"https://api.github.com/users/jozefg/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jozefg/subscriptions","organizations_url":"https://api.github.com/users/jozefg/orgs","repos_url":"https://api.github.com/users/jozefg/repos","events_url":"https://api.github.com/users/jozefg/events{/privacy}","received_events_url":"https://api.github.com/users/jozefg/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/jonsterling/JonPRL/labels/development-state","name":"development-state","color":"bfdadc"},{"url":"https://api.github.com/repos/jonsterling/JonPRL/labels/editor-support","name":"editor-support","color":"d4c5f9"}],"state":"closed","locked":false,"assignee":{"login":"jonsterling","id":55057,"avatar_url":"https://avatars.githubusercontent.com/u/55057?v=3","gravatar_id":"","url":"https://api.github.com/users/jonsterling","html_url":"https://github.com/jonsterling","followers_url":"https://api.github.com/users/jonsterling/followers","following_url":"https://api.github.com/users/jonsterling/following{/other_user}","gists_url":"https://api.github.com/users/jonsterling/gists{/gist_id}","starred_url":"https://api.github.com/users/jonsterling/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jonsterling/subscriptions","organizations_url":"https://api.github.com/users/jonsterling/orgs","repos_url":"https://api.github.com/users/jonsterling/repos","events_url":"https://api.github.com/users/jonsterling/events{/privacy}","received_events_url":"https://api.github.com/users/jonsterling/received_events","type":"User","site_admin":false},"milestone":null,"comments":5,"created_at":"2015-07-01T19:48:29Z","updated_at":"2015-07-16T13:54:46Z","closed_at":"2015-07-15T02:50:19Z","pull_request":{"url":"https://api.github.com/repos/jonsterling/JonPRL/pulls/113","html_url":"https://github.com/jonsterling/JonPRL/pull/113","diff_url":"https://github.com/jonsterling/JonPRL/pull/113.diff","patch_url":"https://github.com/jonsterling/JonPRL/pull/113.patch"},"body":"This solves #109 I believe. The idea is that instead of\r\n\r\n 1. Parsing a world\r\n 2. Checking the proofs\r\n 3. Continuing with the rest of the work\r\n\r\nwhen we evaluate an AST for a development it hands us back a list of `runProof`s, which are functions from `unit -> unit` and are responsible for actually running all the proofs we just gave to `eval`. This doesn't compromise the soundness of JonPRL so long as we run everything because attempting to access the proof a theorem which hasn't yet been forced (via that `evidence` suspension`) will force the proof of the theorem exactly as if we had run it properly in the first place. This does however mean that `evidence` might actually raise an exception if we force it so I've carefully arranged this code to always run handlers before forcing  any evidence.\r\n\r\nNow that `eval` returns a bunch of `runProof`s I have `loadFile` in `ctt_frontend` return another big `runProof` which runs all the proofs in the file top to bottom and carefully pretty prints any errors that arise from this.\r\n\r\nFinally, in `CttFrontend.loadFile` I now accumulate all of these big handlers into a list as we parse each file. This in effect means that by the end `loadFiles` call in `main.sml` we have an option of a world (with no theorems run yet) and a list of functions that will run all the proofs in each file. From there we do all the printing of operators and tactics *and then* trigger run all the theorems.\r\n\r\nOn the other hand this is a bit of a restructuring of the proof assistant so I'd understand if this pull request should be not merged (it will live in my heart forever or something instead).\r\n\r\nTo see this work for listing operators for incomplete developments, you can run `jonprl example/incomplete.jonprl example/test.jonprl --list-operators`. Here `incomplete.jonprl` has outstanding theorems but all the operators get listed and *then* you get the \"'Complete' Failed with goal ...\""},"comment":{"url":"https://api.github.com/repos/jonsterling/JonPRL/issues/comments/121963714","html_url":"https://github.com/jonsterling/JonPRL/pull/113#issuecomment-121963714","issue_url":"https://api.github.com/repos/jonsterling/JonPRL/issues/113","id":121963714,"user":{"login":"jozefg","id":814961,"avatar_url":"https://avatars.githubusercontent.com/u/814961?v=3","gravatar_id":"","url":"https://api.github.com/users/jozefg","html_url":"https://github.com/jozefg","followers_url":"https://api.github.com/users/jozefg/followers","following_url":"https://api.github.com/users/jozefg/following{/other_user}","gists_url":"https://api.github.com/users/jozefg/gists{/gist_id}","starred_url":"https://api.github.com/users/jozefg/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jozefg/subscriptions","organizations_url":"https://api.github.com/users/jozefg/orgs","repos_url":"https://api.github.com/users/jozefg/repos","events_url":"https://api.github.com/users/jozefg/events{/privacy}","received_events_url":"https://api.github.com/users/jozefg/received_events","type":"User","site_admin":false},"created_at":"2015-07-16T13:54:46Z","updated_at":"2015-07-16T13:54:46Z","body":"No worries :) I'll take another crack at it some time!"}}