Timeline
Mar 30, 2011:
- 6:47 PM Changeset [726] by
- Change identifiers to Words in Clight and RTLabs semantics.
- 4:16 PM Changeset [725] by
- Do some light manual disambiguation to make Clight examples go through …
- 2:03 PM Changeset [724] by
- More tractable version of bitvector_of_nat / nat_of_bitvector.
- 12:34 PM Changeset [723] by
- Added dependent type internalising the invariant that LIN function …
Mar 29, 2011:
- 6:32 PM Changeset [722] by
- Committing changes from today. Several files do not typecheck.
- 6:22 PM Changeset [721] by
- Added diary of changes to project files.
- 6:21 PM Changeset [720] by
- Sort out cost labels.
- 6:17 PM Changeset [719] by
- Added missing assembly file ported to matita.
- 5:54 PM Changeset [718] by
- Add an AST type (i.e., intermediate language type) for pointers.
- 5:54 PM Changeset [717] by
- Clean up Clight examples; better temporary definition of multiply.
- 2:29 PM Changeset [716] by
- Finished translating LTL statements to LIN statements. Need to …
- 1:49 PM Changeset [715] by
- Restored rev from Util as it appears that list reversal is not a part …
- 12:24 PM Changeset [714] by
- Work on translation from LTL to LIN.
- 11:48 AM Changeset [713] by
- Commit of initial LTL files.
Mar 28, 2011:
- 5:40 PM Changeset [712] by
- Changes to get things to typecheck.
Mar 27, 2011:
Mar 25, 2011:
- 6:37 PM Changeset [710] by
- Start of way to import RTLabs from prototype compiler.
Mar 23, 2011:
- 4:39 PM Changeset [709] by
- Notations should NOT be redefined. Just add a new interpretation.
- 2:28 PM Changeset [708] by
- Use a more normalize-friendly definition of clight_exec to make the …
- 11:37 AM Changeset [707] by
- Remove old branch, which was merged after the move to src.
- 2:24 AM Changeset [706] by
- Fixed (reference to basics/pairs was dandling).
- 2:21 AM Changeset [705] by
- Ported to new library (notation).
- 2:19 AM Changeset [704] by
- Minor speedup in one theorem (less automation).
Mar 22, 2011:
- 5:42 PM Changeset [703] by
- lib is now the default standard library (after commit 11216 in …
Mar 21, 2011:
- 6:27 PM Changeset [702] by
- Refine small-step executable semantics abstraction a little. Some …
- 5:32 PM Changeset [701] by
- New version.
Mar 18, 2011:
- 4:28 PM Changeset [700] by
- Get Clight semantics going again (except for problems CexecEquiv? that …
- 2:53 PM Changeset [699] by
- More or less finished formalisation of LIN.
- 1:47 PM Changeset [698] by
- Commit with changes to files to get our files to typecheck.
- 1:28 PM Changeset [697] by
- Merge Clight branch of vectors and friends. Start making stuff build.
- 1:01 PM Changeset [696] by
- Added missing I8051 file and completed most of LIN formalisation.
- 12:59 PM Changeset [695] by
- Rearrange Clight files a bit - will try to make them work again soon…
- 12:30 PM Changeset [694] by
- Start moving Clight into common directory.
- 12:11 PM Changeset [693] by
- Separate out whole program executions from the clight semantics and …
- 11:36 AM Changeset [692] by
- Deleted files.
- 11:36 AM Changeset [691] by
- More movement of files within the repository.
- 11:34 AM Changeset [690] by
- Moved new matita files into correct place.
- 11:33 AM Changeset [689] by
- Got rid of old Matita development files.
- 11:31 AM Changeset [688] by
- Fixed local conflicts. Restructured svn repository.
- 11:23 AM Changeset [687] by
- Renamed to enforce consistency of filenames
- 11:22 AM Changeset [686] by
- Most of LIN completed.
Mar 16, 2011:
- 2:36 PM Changeset [685] by
- Bug fix in LINToASM (wrong conditional translation) in 8051 branch.
- 10:14 AM Changeset [684] by
- Moved into Presentations.
Mar 15, 2011:
- 2:47 PM Changeset [683] by
- Changes from working on my PC.
- 2:22 PM Changeset [682] by
- …
- 2:20 PM Changeset [681] by
- …
- 2:19 PM Changeset [680] by
- 8051-memoryspace-branch from Brian moved from D2.3 (that does not …
- 2:13 PM Changeset [679] by
- The one in D2.2/8051 is more up to date. Committing this one was a …
Mar 11, 2011:
- 3:22 PM PublicationVenues edited by
- (diff)
- 9:10 AM Changeset [678] by
- WP-rob update
- 9:05 AM Changeset [677] by
- Use better titles for T3.2/3.3.
Mar 10, 2011:
- 5:46 PM Changeset [676] by
- …
- 4:26 PM Changeset [675] by
- …
- 4:19 PM Changeset [674] by
- …
- 4:10 PM Changeset [673] by
- * Cosmetics.
- 3:16 PM Changeset [672] by
- * Slides shuffling.
- 2:56 PM Changeset [671] by
- Finished demo script for tomorrow.
- 2:50 PM Changeset [670] by
- * New version of the video.
- 2:14 PM Changeset [669] by
- Fixed man months
- 1:46 PM Changeset [668] by
- small changes
- 1:45 PM Changeset [667] by
- Changes to presentation that claudio wanted
- 1:20 PM Changeset [666] by
- WP-roberto update
- 11:52 AM Changeset [665] by
- …
- 11:48 AM Changeset [664] by
- Changed output of Intel HEX files so we no longer have those …
- 9:43 AM Changeset [663] by
- * Video of prototype demonstration.
- 9:39 AM Changeset [662] by
- New version of the slides.
Mar 9, 2011:
- 11:24 PM Changeset [661] by
- Renaming.
- 11:23 PM Changeset [660] by
- Final draft version.
- 10:54 PM Changeset [659] by
- Draft version completed.
- 10:02 PM Changeset [658] by
- …
- 6:11 PM Changeset [657] by
- Mention cost labels in D3.1 summary slide.
- 3:48 PM Changeset [656] by
- rob updated
- 3:35 PM Changeset [655] by
- * Slides from Yann.
- 12:58 AM Changeset [654] by
- In progress
Mar 8, 2011:
- 5:58 PM Changeset [653] by
- New version, still a draft.
- 5:55 PM Changeset [652] by
- Still unfinished.
- 5:40 PM Changeset [651] by
- Small additions to WP3 slides.
- 4:49 PM Changeset [650] by
- Completed presentation slides by mentioning man hours used
- 4:00 PM Changeset [649] by
- Reworked presentation.
Mar 7, 2011:
- 7:00 PM Changeset [648] by
- Oops, wrong bitvector negation.
- 7:00 PM Changeset [647] by
- Minor WP3 edits.
- 5:29 PM Changeset [646] by
- Got Search.ma working with Matita emulator.
- 4:04 PM Changeset [645] by
- Pretty output in D2.2.
- 2:41 PM Changeset [644] by
- Committed files for demo on Friday. Binary search works with O'Caml …
- 2:28 PM Changeset [643] by
- Bug fix in ASMCosts in D2.2.
- 2:19 PM Changeset [642] by
- Added the review example in D2.2 (8051/tests/review1/)
- 2:18 PM Changeset [641] by
- Improvement in the code of the cost computation in D2.2.
- 11:10 AM Changeset [640] by
- Hex output not too long for mcu anymore. Readable output added.
Mar 4, 2011:
- 6:20 PM Changeset [639] by
- Preliminary work on RTLabs semantics Will move to somewhere more …
- 6:20 PM Changeset [638] by
- Switch to more conservative definitions in preparation for review. …
- 6:20 PM Changeset [637] by
- First draft of WP3 slides.
- 6:20 PM Changeset [636] by
- A few definitions that will be useful for some preliminary rtlabs …
- 6:20 PM Changeset [635] by
- Some commentary.
- 5:59 PM Changeset [634] by
- Bug fix in ASMCosts in D2.2.
- 5:38 PM Changeset [633] by
- wp2 revised
- 3:59 PM Changeset [632] by
- Small change in ASMCosts.
- 2:00 AM Changeset [631] by
- Some bugs fixed in D2.2.
Mar 3, 2011:
- 6:27 PM Changeset [630] by
- Paris update in D2.2.
- 4:50 PM Changeset [629] by
- Fixed some slides: added description of WP4.1
- 3:41 PM Changeset [628] by
- Finished slides.
- 1:57 PM Changeset [627] by
- Fixed bug in ASMInterpret.ml. Added pretty printing module.
- 1:29 PM Changeset [626] by
- added draft first part presentation WP2
- 12:57 PM Changeset [625] by
- Fixed ASMInterpret so no assert false is generated. Working on …
Mar 2, 2011:
- 11:06 PM Changeset [624] by
- Bug fixs and signed division hack in D2.2.
- 10:51 PM Changeset [623] by
- - official agenda - new version of the progress report (but the …
- 6:10 PM Changeset [622] by
- Started fixing assert false problem.
- 5:53 PM Changeset [621] by
- Bug fix in cost computation in D2.2.
- 4:13 PM Ticket #3 (Big output code) created by
- Dear all, The compiler now outputs an IntelHex? format. The result …
- 3:57 PM Ticket #2 ([assert false] on branching) created by
- Dear all, When running the compiler on a program with a branch, I get …
- 3:56 PM Changeset [620] by
- More changes to presentation. Modified some of the C examples to test …
- 3:27 PM Changeset [619] by
- Update of D2.2 from Paris.
- 2:19 PM Changeset [618] by
- More work on slides.
- 11:44 AM Changeset [617] by
- Fixed layout.
- 11:40 AM Changeset [616] by
- More changes.
- 11:07 AM Changeset [615] by
- Work on presentation.
Mar 1, 2011:
- 6:12 PM Changeset [614] by
- Template for the presentation.
- 5:47 PM Changeset [613] by
- More changes to skeleton.
- 5:15 PM Changeset [612] by
- Moved presentation file to something more descriptive.
- 5:04 PM Changeset [611] by
- Added my skeleton presentation file for first-year meeting.
- 4:59 PM Changeset [610] by
- Added directory for the presentations for the first-year meeting with …
- 3:47 PM Changeset [609] by
- …
- 1:07 PM Changeset [608] by
- Final changes to document to get first section under 4 pages.
- 12:51 PM Changeset [607] by
- Finished correcting English in the introduction
- 11:59 AM Changeset [606] by
- Changes to English in intro to report.
Feb 28, 2011:
Note: See TracTimeline
for information about the timeline view.
