Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

Lean in Orsay, 2018

Jump to bottom
Scott Morrison edited this page Aug 24, 2018 · 3 revisions

  • Upcoming PRs, e.g. (cf https://goo.gl/Lqcor7)

    • Which ones need help?
    • Which ones need discussion of design decisions?
    • Which ones need coordination between parallel efforts?
    • Write some code!
    • Tentative list of current upcoming PRs:
      • category theory (Scott, Reid, Kenny)
      • sheaf theory
      • commutative algebra scattered in various repos (Kenny)
      • homology (Johan)
      • norms (Patrick)
      • smooth manifolds (Patrick)
      • ...?

  • Documentation push

    • Ed Ayers' draft meta-programming docs
    • ...?

  • Teaching materials for Lean

  • Community processes

    • Is the leanprover-community fork working?
    • How can we lessen the burden on Mario and Johannes merging PRs, while maintaining standards?

  • Further automation for mathlib

    • Improving find.
    • Getting tidy and rewrite_search in shape for mathlib.
      • tidy just needs cleaning up, but this seems very doable.
      • rewrite_search is designed to be modular, so you can plug in different strategies. The modular design needs adjusting, but after that is done it seems plausible to get a "working" version of rewrite_search into mathlib, and leave optimising the strategies in user space.
    • A version of to_additive that saves having to write all the dual notions separately in category theory.
    • Are there some basic decision procedure tactics that we should line up as student projects for Lean?

  • Infrastructure

    • All-in-one windows installer
    • Linter
    • Hole commands in IDEs
    • Parsing and presenting error traces (e.g. instance resolution)
    • Visualisation of terms (e.g. collapsible substructures, identifying repeats, colour coding)
    • Scalability of continuous integration on travis
    • leanpkg
      • leanpkg clean
      • leanpkg tracking specified branches
      • leanpkg installing olean files

  • Partial formalisations of significant modern results

    • Formal abstracts is slow to get started
    • Should we do some of this?
    • Should it be in mathlib, even with sorry?
    • Targets?
Clone this wiki locally