AIMXVICodeSprint

Code Sprint Discussions.

• Colors in Agda
  (discussion sprint on Polychromatic TT, as means to get parametricity and much more.)
  • JP, NAD, AA, GM, UN, BM, JC, NP, SA, DF
  • Day 2:
    Begining hacking. Modest Plan. List to Nat. Simple case working for closed code. Looking at code dealing with irrelevance, since color would be dealt in similar places. Guillem Changing code now. Color variables and quantification over colors. Syntax still under discussion.
  • Day 3: Continued hacking; parser done, some beginning of typechecking.
  • Day 6: New input from AA and NAD, clearer goal know, and how to do it. Still more to do.
  • Day 7 Propagating current changes to every single module. ~50% done. (Then the actual typing rules can start to be implemented)
• Doc, Manual
  • JC, YK
  • Day 2:
    Updated Agda Wikipedia page. Started maintaining old tutorial. Nothing on manual.
  • Day 3: There are more references in the tutorial; it's published on the interblargs.
  • Day 6: Wikipedia reverted previous change due to copyright violation???
  • Day 7: More conservative edit to Wikipedia done. Imported the release notes to the manual. SUCCESS!
• Pattern matching and case expression (what's the problem etc.)
  • JP, NAD, JC, AA, BN, UN
  • Day 2:
    Discussion on PM. Main problem: continuous case splitting works interactively but fails on reload. Sol: Looking at patterns in clauses as matrix and look for a column which is a covering. No impl.
  • Day 3: Andreas has implemented split trees, but they are not connected to anything. Splitting algorithm not implemented. NAD: demo of parallel/simultaneous case-split. Pushed to the repo.
  • Day 6: Algorithm is clear, but some obstacles on the way. Fiddling in coverage-checker. Getting clause compilation for record patterns.

     The pipeline : Coverage check, generating split-tree, compile clauses phase and then move record patterns.

• Day 7: Finished record pattern translation for split-trees. Need to fix coverage checking for literals before making further progress. Taking the sprint home. NOTE: being an empty string is an undecidable property currently.

• Improving instance argument. Implicit calculus
  • SK, AA
  • Day 2:
  Discussion only.
  • Day 3,6,7: Nothing
• Windows Installer
  • MT
  • Day 2: In the middle of updating to Platform 2012.2.0.0, emacs-24.2, ... Not working yet.
  • Day 3: Testing underway.
• Copatterns in core
  • BN, DG, AA, NAD, JC, DF, JP, YK, MB, UN
  • Day 2:
    A lot of discussion together with "Sized types". Copatterns approved!
  • Day 3, 6: nothing
• Sized types
  • AA, NAD, DF, JP, NP, UN, MB, GM
  • Day 2:
    A lot of discussion. Don't want to write or see size vars. Developed into discussion on Twelf like auto quantification.
  • Day 3, 6: Nothing
  • Day 7: Discussed the relation between Sized types and Guarded types.
• Liberate Agda from Emacs
  • PD, SA, SK, BN
  • Day 2: presentation of a working web-frontend prototype with basic editing, type-checking and "give" command support
    Demo on Agda server. Accessing localhost:8001/X.xml loads module X.agda. If X is not present already, skelton module is created. Free-form editing in a large form. Pressing check botton shows the error messages on the same page. Each loaded module has its own Agda state. [Nisse: sharing is better for speed and memory]. X.xml cotaining automatically generated identifiers for XXX and generated javascript to invoke the server. Idea: Domain specific language for describing the interaction with the server. [Nisse: forcing structured editing would be annoying] XXX [JP: Imagine Agda version of Wikipedia] DSL for interaction has a lot of potential. Emacs interface is too limited. A monad generates javascript as side effect of making definitions ...
  • Day 3: begin work on a model in which interactive coding can be described
    The model should be expressive enough but the simpler the better. The initial model has a screen with a box tree with a focus (or a selection/cursor is better). Keyboard shortcuts are attached to nodes of the box tree and leafs are either labels or text input areas. The users see the rendered box tree. Keyboard shortcuts may be rendered as buttons. The source code is a special kind of rendering of the box tree. Keyboard shortcuts has attached events which may change the screen and the Agda compiler state. Events which change the screen only should not connect the server for efficiency reasons. This is possibly expressible by the Haskell type system.
    Open questions
    • [MT] level of granuality (every word is an individual input area?)
    • [NAD] can we guarantee somehow that the screen is in sync with the Agda compiler state?
  • Day 6: Still working on interface to the compiler.
• Faster emacs mode with COCOA emacs.
  • GM, JC, NAD
  • Day 2:
    Nothing
  • Day 3:
    The current patch isn't complete yet; but gives you a MASSIVE speedup under cocoa.
  • Day 6: patch pushed, reduced flickering FIXED! :)
• Sharing (call by need)
  • UN, NP, NAD, DG, AA, MT
  • Day 2:
    Resumed from the last summer's attempt. Fixed the new code since then. With sharing turned on, not so slower than the no sharing. Probably because there really is little sharing with current code. Still lots more improvement possible.
  • Day 3:

     We found out why the pointers were disappearing. We now have pointers (307400 of them). We fixed more bugs. Sharing still makes things slower and uses more memory. It's currently not clear what to do to improve the situation.

• Day 6: We have started figure out where we lose sharing. When metavar gets instantiated we check variables that are in scope. This check makes us currently lose sharing. Some hackery allows us to get around some of this. Slowly we figure out how to do this.

  * Day 7: If you check syntactic equality before unification, you actually gain surprisingly much. (Saves maybe 10% in the std. library typechecking time). We've identified that De Bruijn indices are messing up sharing. Annoying! What can we do? Maybe explicit substitutions; Maybe keep track of closed terms (so substituting in a closed term is a noop and keeps sharing). We are going to run more experiments. 

• Syntax improvement
  x y : T x = ... y = ...
  • Day 2,3: Nothing
  • Day 6: One line "solution" doesn't work, (gives reduce/reduce errors). Trying to be more principle in the solution, we might have a pass from Concrete to Concrete. UN: There should already be such a pass? UN: go ahead and duplicate the types and internally make more type sigs.

In a real solution we shouldn't duplicate work (type checking etc.) AA: there is also some problems if we get more metavariable.

  * Day 7: Done, pushed, documented and tested. SUCCESS! 

• Bug fix
  • AA, GM, SK, JC
  • (AA: 50026)
  • Day 2:
    Nothing
  • Day 3:
    We now have a patch where the meta variables are named and you can even see them in error messages; but not in constraints yet.
  • Day 4: Fixed and pushed! SUCCESS!
• Vague notion.\\ (Nisse: at the last ITP "large enough" was discussed in Coq.)
  • YK, BN, MT
  • Day 2:
    Point would be to restrict the power of induction. Coding PA- (PA minus induction) in Agda.
  • Day 3:
    YK: Try to formalise the goal in Agda. Discussion is going on to clarify the meaning. Maybe the sandhill example is confusing. Nad: 1+1=1, in sandhill units. Main idea: there exists a big quantity which is not reachable from zero. BN: Is this related to induction on ordinals? YK: the set of interest should not be inductively defined.
• Fold and Unfold definition in emacs.
  (JP: there's something fundamental about how much you want your terms to be reducible.
  Nisse: Possibly a library. Like Inspect
  Nicolas: In Coq, mode-dependent. In proof-mode, all manual.
  Ulf: influences on sharing.
  Nisse: and on compilation. Possibly keeping both normalised and unnormalised.
  )
  • Day 2-7:
    No progress
• Sharing optimisation with Epic
  • DG, AA
  • Day 2:
    Talking with Ulf. Seems feasible.
  • Day 3: Starting to fix some bugs in the epic backend.
  • Day 5:

     Fixed some bugs in the epic backend.

• Day 6: Nothing

  * Day 7: Study of MAlonzo.

• Outside code-sprint
  • Day 6: James has added an better error-message for ambiguous module name. (DEMO)
  • Day 7: James: fixed bug 318