Search:
Login
Preferences
Help/Guide
About Trac
Wiki
Timeline
Roadmap
Browse Source
View Tickets
Search
Context Navigation
View Latest Revision
source:
extracted
Revision Log Mode:
Stop on copy
Follow copies
Show only adds and deletes
View log starting at
and back to
Show at most
revisions per page.
Show full log messages
Legend:
Added
Modified
Copied or renamed
Diff
Rev
Age
Author
Log Message
(edit)
@2803
8 years
sacerdot
More code extracted, used to debug the compiler.
(edit)
@2797
8 years
sacerdot
Extracted again after James's cleanup and the implementation of the …
(edit)
@2789
8 years
campbell
Some changes to the driver to aid debugging.
(edit)
@2780
8 years
sacerdot
Bug fixed: in
BitVector?
.ma the functions bv_to_nat and nat_to_bv were …
(edit)
@2777
8 years
sacerdot
One computational daemon closed.
(edit)
@2775
8 years
sacerdot
The compiler now computes also the stack cost model.
(edit)
@2773
8 years
sacerdot
1. everything extracted again after all bugs in Matita's extraction …
(edit)
@2759
8 years
campbell
Print out costs, with choice of style. Note small anti-assertion patch …
(edit)
@2746
8 years
sacerdot
1. debugging code in glue 2. updated version
(edit)
@2743
8 years
sacerdot
Latest version of the compiler, extracted with the latest version of …
(edit)
@2742
8 years
sacerdot
Untrusted register colouring fully branched.
(edit)
@2740
8 years
sacerdot
Graph colouring terminated up to Uses that will be implemented in Matita.
(edit)
@2738
8 years
sacerdot
Porting the graph colouring stuff from the untrusted prototype to the …
(edit)
@2736
8 years
sacerdot
Untrusted fixpoint computation branched in.
(edit)
@2733
8 years
sacerdot
All axioms in set_adt implemented by hand.
(edit)
@2731
8 years
sacerdot
Minimal set of axioms implemented to make the driver run.
(edit)
@2730
8 years
sacerdot
Exported again.
(edit)
@2719
8 years
sacerdot
More values manually abstracted to functions to avoid failwiths at …
(edit)
@2718
8 years
sacerdot
set_empty turned from a value to a function because it is not …
(edit)
@2717
8 years
sacerdot
Extracted code for the whole compiler. The space cost model is not …
(edit)
@2649
8 years
sacerdot
…
(edit)
@2636
8 years
campbell
Extracted front-end.
(edit)
@2620
8 years
campbell
Sufficient hacking to run the extracted Clight semantics.
(edit)
@2602
8 years
piccolo
Dead code commented out.
(add)
@2601
8 years
sacerdot
Extraction to ocaml is now working, with a couple of bugs left. One …
Note:
See
TracRevisionLog
for help on using the revision log.
Download in other formats:
RSS Feed
ChangeLog