Timeline
Apr 12, 2011:
- 12:32 PM Changeset [750] by
- Track some of the changes to the prototype in RTLabs. Just one …
- 12:32 PM Changeset [749] by
- Make definition more explicit to avoid jmeq.
- 12:32 PM Changeset [748] by
- Change example statement for easier testing.
Apr 8, 2011:
- 2:06 PM Changeset [747] by
- Merge the two AST files together (although some definitions still need …
- 11:51 AM Changeset [746] by
- Changes to bitvectortrieset: equality on sets. Added new file for …
- 10:15 AM Changeset [745] by
- Changes from yesterday. Slowly implementing the functorized …
Apr 7, 2011:
- 6:53 PM Changeset [744] by
- Evict Coq-style integers from common/Integers.ma. Make more bitvector …
- 11:11 AM Changeset [743] by
- Removed mess from yesterday.
Apr 6, 2011:
- 11:16 AM Changeset [742] by
- Added extra debugging feature for Nicolas
Apr 4, 2011:
- 6:24 PM Changeset [741] by
- Bug fix in LINToASM in D2.2's 8051 (negative integers).
- 5:18 PM Changeset [740] by
- New memory model and bug fixes in 8051 branch. Added primitive …
- 5:16 PM Changeset [739] by
- Note on identifiers in CHANGES.
- 5:13 PM Changeset [738] by
- Use lower case names for identifiers for consistency with CompCert? …
- 5:13 PM Changeset [737] by
- Use more abstract identifiers in Clight / RTLabs.
- 5:13 PM Changeset [736] by
- Extra type safety for identifiers.
Apr 1, 2011:
- 6:12 PM Changeset [735] by
- Changes from today
- 4:14 PM Changeset [734] by
- Fixed lin2asm.
- 4:09 PM Changeset [733] by
- Fixed partial commit.
- 2:52 PM Changeset [732] by
- Fixups for CexecEquiv? due to earlier changes in SmallstepExec?.ma
- 1:35 PM Changeset [731] by
- Common definition for animation semantics, and factor out IO definitions.
- 12:03 PM Changeset [730] by
- A few deviations from the prototype / CompCert? that I can think of offhand.
- 12:03 PM Changeset [729] by
- Pretty ugly printer for RTLabs programs.
Mar 31, 2011:
- 5:53 PM Changeset [728] by
- Changes from last two days.
- 5:20 PM Changeset [727] by
- Enough fixes to let an RTLabs program run.
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 …
Note: See TracTimeline
for information about the timeline view.
