Commits

Branch selector

 master

User selector

All users

All time

Commit History

Commits on Nov 1, 2018

• [WIP] fix update and add some flesh to backward simulation lemmas

  cipher1024

  committed
  accec04

  Copy full SHA for accec04

Commits on Oct 16, 2018

• more stuff

  cipher1024

  committed
  3225d26

  Copy full SHA for 3225d26

Commits on May 28, 2018

• [WIP] upgrade to Lean 3.4.1

  cipher1024

  committed
  890c27e

  Copy full SHA for 890c27e

Commits on Apr 15, 2018

• port build to Elan

  cipher1024

  committed
  e219c8a

  Copy full SHA for e219c8a

Commits on Mar 29, 2018

• fix(test_suite)

  cipher1024

  committed
  57186a3

  Copy full SHA for 57186a3

• perf(explicit): further optimization and fixes

  cipher1024

  committed
  caa17b2

  Copy full SHA for caa17b2

• perf(tactic): `explicit'` calls `simp` fewer times. Should reduct on the compile time of the rule list

  cipher1024

  committed
  27719e3

  Copy full SHA for 27719e3

Commits on Mar 25, 2018

• encode names as raw strings in canonical temporal logic sequents

  cipher1024

  committed
  e92b332

  Copy full SHA for e92b332

• introduce an encoding to make `intro` faster and minimize the switching to and from that encoding

  cipher1024

  committed
  b26969e

  Copy full SHA for b26969e

Commits on Mar 24, 2018

• make `save_info` lazier and performance measurements

  cipher1024

  committed
  d256158

  Copy full SHA for d256158

Commits on Mar 21, 2018

• [skip-ci] use a more standard format for org-mode tables

  cipher1024

  committed
  f21cfd2

  Copy full SHA for f21cfd2

• add a simp attribute `tl_simp` to use in `[temporal]` mode. This is an attempt at improving the performances of temporal proofs

  cipher1024

  committed
  d2a0f3c

  Copy full SHA for d2a0f3c

Commits on Mar 15, 2018

• upgrade Lean, `mathlib` and `lean-lib`

  cipher1024

  committed
  3ab869e

  Copy full SHA for 3ab869e

Commits on Feb 21, 2018

• applied the renaming of `auto` / `solve_by_elim` and `xassumption` / `apply_assumption`

  cipher1024

  committed
  3c03ea0

  Copy full SHA for 3c03ea0

Commits on Feb 18, 2018

• Added instances for inferring schedulability of sets of events

  cipher1024

  committed
  ad45fe4

  Copy full SHA for ad45fe4

Commits on Feb 17, 2018

• deleted dead code

  cipher1024

  committed
  4b1e344

  Copy full SHA for 4b1e344

• filled in details for inductive rule of "infinitely often implies infinitely often" properties

  cipher1024

  committed
  2e85fce

  Copy full SHA for 2e85fce

Commits on Feb 16, 2018

• filled in lemmas

  cipher1024

  committed
  72cfa5d

  Copy full SHA for 72cfa5d

• in refinement.simulation, assumption about abstract invariant is formulated in terms of its inductive proof

  cipher1024

  committed
  0e572a5

  Copy full SHA for 0e572a5

Commits on Feb 15, 2018

• filled in lemma for abstract invariants in many-to-many refinement

  cipher1024

  committed
  f857ef9

  Copy full SHA for f857ef9

Commits on Feb 14, 2018

• added the option of assuming guards and abstract invariant in proofs of simulation

  cipher1024

  committed
  16f3378

  Copy full SHA for 16f3378

Commits on Feb 12, 2018

• filled in the scheduling part of one-to-one refinement and many-to-many refinement

  cipher1024

  committed
  9d6a11a

  Copy full SHA for 9d6a11a

Commits on Feb 11, 2018

• Upgraded Lean

  cipher1024

  committed
  89d7f14

  Copy full SHA for 89d7f14

Commits on Feb 10, 2018

• filled in lemmas in the proof of scheduling

  cipher1024

  committed
  39fd056

  Copy full SHA for 39fd056

• changed the approach in scheduling to rely on a surjective queue rather than injective numbering function

  cipher1024

  committed
  12de377

  Copy full SHA for 12de377

Commits on Feb 6, 2018

• Extracted lemmas in proof of scheduling

  cipher1024

  committed
  0c18ce4

  Copy full SHA for 0c18ce4

• filled in lemma about non-increasing queue rank in the scheduler

  cipher1024

  committed
  babf56b

  Copy full SHA for babf56b

Commits on Feb 5, 2018

• Filled in proof of invariance of `injective q`

  cipher1024

  committed
  a665877

  Copy full SHA for a665877

Commits on Feb 3, 2018

• In scheduling, completed proof that each event's rank in a queue decreases

  cipher1024

  committed
  7e7cee1

  Copy full SHA for 7e7cee1

• filled in a `sorry` and fixed `explicit'` to clear in the reverse order of constant dependency

  cipher1024

  committed
  527ade1

  Copy full SHA for 527ade1

• changed `monotonicity only` for `monotonicity!` which denotes that the context will be made persistent before using monotonicity (`!` suggests more aggressive)

  Show description for 6a6d781
  cipher1024

  committed
  6a6d781

  Copy full SHA for 6a6d781

Commits on Feb 2, 2018

• fixed test case, made `split` only optionally aggressive

  cipher1024

  committed
  7e6e0ea

  Copy full SHA for 7e6e0ea

• Sketched a proof that a given set of events is schedulable

  cipher1024

  committed
  6f20a28

  Copy full SHA for 6f20a28

Commits on Feb 1, 2018

• added a specification for the feasibility of scheduling

  cipher1024

  committed
  c0026f1

  Copy full SHA for c0026f1

Commits on Jan 31, 2018

• Added some scheduling information in assumptions to weaken them

  cipher1024

  committed
  98eff83

  Copy full SHA for 98eff83

Pagination

Previous

Next