|
|
|
@1912
|
8 years |
mulligan |
Patches to get block_cost' and dependencies working again after change …
|
|
|
|
@1911
|
8 years |
mulligan |
Changed statement of block_cost' to start on new termination argument
|
|
|
|
@1910
|
8 years |
mulligan |
Finished proof modulo termination argument
|
|
|
|
@1909
|
8 years |
mulligan |
Ported new statements to remainder of Interpret.ma file.
|
|
|
|
@1907
|
8 years |
mulligan |
Fixes to get file to compile
|
|
|
|
@1906
|
8 years |
mulligan |
Statements simplified in block_cost and dependencies
|
|
|
|
@1904
|
8 years |
mulligan |
Problem with proof fixed by noting that problem is actually irrelevant
|
|
|
|
@1903
|
8 years |
mulligan |
Small changes prior to experiment
|
|
|
|
@1902
|
8 years |
mulligan |
Reverted needless changes to StructuredTraces?
|
|
|
|
@1901
|
8 years |
mulligan |
Slight changes to StructuredTraces?: should not change too much
|
|
|
|
@1895
|
8 years |
mulligan |
Split the ASMCosts files while working on traverse_code_internal. A …
|
|
|
|
@1894
|
8 years |
mulligan |
Closed a hole in the proof by deriving a contradiction using even_p …
|
|
|
|
@1892
|
8 years |
mulligan |
Lots of work from today
|
|
|
|
@1891
|
8 years |
mulligan |
Nightmarish proofs on bitvectors. Trying to find some way of making …
|
|
|
|
@1869
|
8 years |
mulligan |
a load of axioms closed in ASMCosts file
|
|
|
|
@1831
|
8 years |
mulligan |
small changes to asmcosts file to refactor proof
|
|
|
|
@1807
|
8 years |
mulligan |
some changes, as finally worked out what i was up to prior to working …
|
|
|
|
@1711
|
8 years |
mulligan |
finished block_cost' proof: 1.5 minutes to typecheck qed.
|
|
|
|
@1710
|
8 years |
mulligan |
changes from friday afternoon
|
|
|
|
@1709
|
8 years |
mulligan |
Changes to the execution of the MOVC instruction
|
|
|
|
@1697
|
8 years |
mulligan |
important bug found
|
|
|
|
@1696
|
8 years |
mulligan |
finished adding russell types to the traverse_cost_* functions
|
|
|
|
@1693
|
8 years |
mulligan |
Changes to ASMCosts and CostsProofs? files to get everything working again.
|
|
|
|
@1692
|
8 years |
mulligan |
resolved conflict in asm costs this morning
|
|
|
|
@1691
|
8 years |
sacerdot |
Some progress in the proof: less daemons, less hypotheses in lemmas.
|
|
|
|
@1684
|
8 years |
mulligan |
changes from the past week
|
|
|
|
@1669
|
8 years |
mulligan |
Commit for claudio
|
|
|
|
@1665
|
8 years |
mulligan |
progress on closing holes in block_cost' proof
|
|
|
|
@1663
|
8 years |
mulligan |
old cases working again, work on new ones
|
|
|
|
@1658
|
8 years |
mulligan |
asm costs changes from today
|
|
|
|
@1650
|
8 years |
mulligan |
changes over the last couple of days: stuck due to matita producing …
|
|
|
|
@1648
|
8 years |
mulligan |
new version of utilities/monad.ma with typecheck command comented out
|
|
|
|
@1646
|
8 years |
mulligan |
finished the block_costs computation, and propagated the changes …
|
|
|
|
@1645
|
8 years |
mulligan |
more progress on the ASMCosts work: block_costs is now complete …
|
|
|
|
@1642
|
8 years |
mulligan |
finished big proof in all but two cases
|
|
|
|
@1639
|
8 years |
mulligan |
changes from today
|
|
|
|
@1625
|
8 years |
mulligan |
before christmas
|
|
|
|
@1624
|
8 years |
mulligan |
commit for claudio
|
|
|
|
@1623
|
8 years |
mulligan |
strange matita issue
|
|
|
|
@1622
|
8 years |
mulligan |
to avoid conflicts, bug in typechecker?
|
|
|
|
@1621
|
8 years |
mulligan |
to prevent conflicts
|
|
|
|
@1606
|
8 years |
sacerdot |
Porting to last library of Matita.
|
|
|
|
@1597
|
8 years |
mulligan |
fixed fetch for jaap
|
|
|
|
@1591
|
8 years |
mulligan |
work from today
|
|
|
|
@1587
|
8 years |
mulligan |
changes from today, including removing indexing of problematic …
|
|
|
|
@1560
|
8 years |
sacerdot |
Complete re-implementation that:
1) assumes no code before the first …
|
|
|
|
@1557
|
8 years |
sacerdot |
Byte => costlabel
|
|
|
|
@1497
|
8 years |
mulligan |
a bit of tidying up, removing dead code, etc.
|
|
|
|
@1496
|
8 years |
mulligan |
problem fixed with tactics missing a semicolon to stop greedy parsing
|
|
|
|
@1495
|
8 years |
mulligan |
proper calculation of costs
|
|
|
|
@1486
|
8 years |
mulligan |
finished asm costs
|
|
|
|
@1474
|
8 years |
mulligan |
adding missing asmcosts file for computing the costs of an assembly …
|
