purplecat: Hand Drawn picture of a Toy Cat (Default)
Achieved:

  • Established that B. was well enough to get G. to school and can now walk without crutches. Re-assured that they won't starve before I get back I have stuck by my original plan to return home tomorrow evening.

  • Talked to DA. This involved installing yet another version of emacs, a new version of proof general, three new versions of Isabelle and a new version of IsaPlanner and then patching the preferred configuration. Just got an email from DA asking rather plaintively if we could actually discuss research tomorrow rather than installation issues.

  • Got IsaPlanner to perform a middle-out reasoning proof, but did this interactively and revealed a nice big search space. Agreed that since middle-out reasoning is a major part of MJo's thesis project she would look at the implications of handling the search space and I would carry on in interactive mode.

  • Went to a talk on parallelising Computer Algebra - this won me a free lunch.

  • Wrote a draft Blue book note on proof specification languages.



To Do:

  • Integrate middle-out reasoning proof with a critic.

  • Finish Blue book note.

  • Get taken to dinner by group.

purplecat: Hand Drawn picture of a Toy Cat (Default)
Achieved:


  • JG sent me a PDF of our note on proof specification languages: read but not digested.

  • Asked LD about putting induction challenge problems into TPTP THF - LD agrees with my approach. LD tried to check type definitions in IsaPlanner for me: "unfortunately most of my systems are halfway between broken and working... which means they're broken".

  • Installed latest versions of both Isabelle and IsaPlanner.

  • Installed Aquaemacs because LD's sml-mode doesn't work in xemacs on the Mac

  • Worked out how to use IsaPlanner using Aqaemacs - it was about 3pm when we got to this point. Getting everything
    set up was slow work not helped by the fact LD had food poisoning and didn't appear until midday leaving MJo and I flailing around rather.

  • Created a handout for my dream talk.

  • Started writing a critic for IsaPlanner - stalled firstly because Isabelle won't let me use partial definitions in the simplifier and then later because there is no way to remove rules from IsaPlanner's wave rule database (which would bypass the simplifier). LD was about to start working on this when South Central Edinburgh blacked out. I'm now in an Internet cafe on the lighted side of Nicholson Street.

  • Observed the introduction of new "stylish" furniture to the Dream group communal areas. Listened to the departmental administrator curse architects and various others compare the furniture unflatteringly to contemporary bars and airport lounges.

  • Discovered that Appleton Tower has extremely poor emergency lighting in the stairwell.



To do:


  • Still no sign of DA

  • Decide what to say in my dream talk

  • Actually Implement that critic

  • Discuss proof plan specification languages further with LD.

Profile

purplecat: Hand Drawn picture of a Toy Cat (Default)
purplecat

June 2017

S M T W T F S
    123
45678 9 10
11 12 13 14 1516 17
18 19 20 21222324
252627282930 

Syndicate

RSS Atom

Tags

Style Credit

Expand Cut Tags

No cut tags