

@2844

9 years 
piccolo 
Stupid bug fixed



@2842

9 years 
sacerdot 
The compiler can now show all backend traces too (assembly and object …



@2836

9 years 
sacerdot 
…



@2833

9 years 
sacerdot 
…



@2831

9 years 
sacerdot 
…



@2829

9 years 
sacerdot 
Semantics files committed.



@2827

9 years 
sacerdot 
Everything extracted again.



@2812

9 years 
sacerdot 
Preclassified system for RTLabs.



@2810

9 years 
sacerdot 
Cminor semantics exported.



@2803

9 years 
sacerdot 
More code extracted, used to debug the compiler.



@2797

9 years 
sacerdot 
Extracted again after James's cleanup and the implementation of the …



@2789

9 years 
campbell 
Some changes to the driver to aid debugging.



@2780

9 years 
sacerdot 
Bug fixed: in BitVector?.ma the functions bv_to_nat and nat_to_bv were …



@2777

9 years 
sacerdot 
One computational daemon closed.



@2775

9 years 
sacerdot 
The compiler now computes also the stack cost model.



@2773

9 years 
sacerdot 
1. everything extracted again after all bugs in Matita's extraction …



@2759

9 years 
campbell 
Print out costs, with choice of style.
Note small antiassertion patch …



@2746

9 years 
sacerdot 
1. debugging code in glue
2. updated version



@2743

9 years 
sacerdot 
Latest version of the compiler, extracted with the latest version of …



@2742

9 years 
sacerdot 
Untrusted register colouring fully branched.



@2740

9 years 
sacerdot 
Graph colouring terminated up to Uses that will be implemented
in Matita.



@2738

9 years 
sacerdot 
Porting the graph colouring stuff from the untrusted prototype to the …



@2736

9 years 
sacerdot 
Untrusted fixpoint computation branched in.



@2733

9 years 
sacerdot 
All axioms in set_adt implemented by hand.



@2731

9 years 
sacerdot 
Minimal set of axioms implemented to make the driver run.



@2730

9 years 
sacerdot 
Exported again.



@2719

9 years 
sacerdot 
More values manually abstracted to functions to avoid failwiths at …



@2718

9 years 
sacerdot 
set_empty turned from a value to a function because it is not …



@2717

9 years 
sacerdot 
Extracted code for the whole compiler.
The space cost model is not …



@2649

9 years 
sacerdot 
…



@2636

9 years 
campbell 
Extracted frontend.



@2620

9 years 
campbell 
Sufficient hacking to run the extracted Clight semantics.



@2602

9 years 
piccolo 
Dead code commented out.



@2601

9 years 
sacerdot 
Extraction to ocaml is now working, with a couple of bugs left.
One …
