Timeline



Apr 8, 2011:

2:06 PM Changeset [747] by campbell
Merge the two AST files together (although some definitions still need …
11:51 AM Changeset [746] by mulligan
Changes to bitvectortrieset: equality on sets. Added new file for …
10:15 AM Changeset [745] by mulligan
Changes from yesterday. Slowly implementing the functorized …

Apr 7, 2011:

6:53 PM Changeset [744] by campbell
Evict Coq-style integers from common/Integers.ma. Make more bitvector …
11:11 AM Changeset [743] by mulligan
Removed mess from yesterday.

Apr 6, 2011:

11:16 AM Changeset [742] by mulligan
Added extra debugging feature for Nicolas

Apr 4, 2011:

6:24 PM Changeset [741] by ayache
Bug fix in LINToASM in D2.2's 8051 (negative integers).
5:18 PM Changeset [740] by ayache
New memory model and bug fixes in 8051 branch. Added primitive …
5:16 PM Changeset [739] by campbell
Note on identifiers in CHANGES.
5:13 PM Changeset [738] by campbell
Use lower case names for identifiers for consistency with CompCert?
5:13 PM Changeset [737] by campbell
Use more abstract identifiers in Clight / RTLabs.
5:13 PM Changeset [736] by campbell
Extra type safety for identifiers.

Apr 1, 2011:

6:12 PM Changeset [735] by mulligan
Changes from today
4:14 PM Changeset [734] by mulligan
Fixed lin2asm.
4:09 PM Changeset [733] by mulligan
Fixed partial commit.
2:52 PM Changeset [732] by campbell
Fixups for CexecEquiv? due to earlier changes in SmallstepExec?.ma
1:35 PM Changeset [731] by campbell
Common definition for animation semantics, and factor out IO definitions.
12:03 PM Changeset [730] by campbell
A few deviations from the prototype / CompCert? that I can think of offhand.
12:03 PM Changeset [729] by campbell
Pretty ugly printer for RTLabs programs.

Mar 31, 2011:

5:53 PM Changeset [728] by mulligan
Changes from last two days.
5:20 PM Changeset [727] by campbell
Enough fixes to let an RTLabs program run.

Mar 30, 2011:

6:47 PM Changeset [726] by campbell
Change identifiers to Words in Clight and RTLabs semantics.
4:16 PM Changeset [725] by campbell
Do some light manual disambiguation to make Clight examples go through …
2:03 PM Changeset [724] by campbell
More tractable version of bitvector_of_nat / nat_of_bitvector.
12:34 PM Changeset [723] by mulligan
Added dependent type internalising the invariant that LIN function …

Mar 29, 2011:

6:32 PM Changeset [722] by mulligan
Committing changes from today. Several files do not typecheck.
6:22 PM Changeset [721] by mulligan
Added diary of changes to project files.
6:21 PM Changeset [720] by campbell
Sort out cost labels.
6:17 PM Changeset [719] by mulligan
Added missing assembly file ported to matita.
5:54 PM Changeset [718] by campbell
Add an AST type (i.e., intermediate language type) for pointers.
5:54 PM Changeset [717] by campbell
Clean up Clight examples; better temporary definition of multiply.
2:29 PM Changeset [716] by mulligan
Finished translating LTL statements to LIN statements. Need to …
1:49 PM Changeset [715] by mulligan
Restored rev from Util as it appears that list reversal is not a part …
12:24 PM Changeset [714] by mulligan
Work on translation from LTL to LIN.
11:48 AM Changeset [713] by mulligan
Commit of initial LTL files.

Mar 28, 2011:

5:40 PM Changeset [712] by mulligan
Changes to get things to typecheck.

Mar 27, 2011:

3:06 PM Changeset [711] by sacerdot

Mar 25, 2011:

6:37 PM Changeset [710] by campbell
Start of way to import RTLabs from prototype compiler.

Mar 23, 2011:

4:39 PM Changeset [709] by sacerdot
Notations should NOT be redefined. Just add a new interpretation.
2:28 PM Changeset [708] by campbell
Use a more normalize-friendly definition of clight_exec to make the …
11:37 AM Changeset [707] by campbell
Remove old branch, which was merged after the move to src.
2:24 AM Changeset [706] by sacerdot
Fixed (reference to basics/pairs was dandling).
2:21 AM Changeset [705] by sacerdot
Ported to new library (notation).
2:19 AM Changeset [704] by sacerdot
Minor speedup in one theorem (less automation).

Mar 22, 2011:

5:42 PM Changeset [703] by sacerdot
lib is now the default standard library (after commit 11216 in …

Mar 21, 2011:

6:27 PM Changeset [702] by campbell
Refine small-step executable semantics abstraction a little. Some …
5:32 PM Changeset [701] by sacerdot
New version.

Mar 18, 2011:

4:28 PM Changeset [700] by campbell
Get Clight semantics going again (except for problems CexecEquiv? that …
2:53 PM Changeset [699] by mulligan
More or less finished formalisation of LIN.
1:47 PM Changeset [698] by mulligan
Commit with changes to files to get our files to typecheck.
1:28 PM Changeset [697] by campbell
Merge Clight branch of vectors and friends. Start making stuff build.
1:01 PM Changeset [696] by mulligan
Added missing I8051 file and completed most of LIN formalisation.
12:59 PM Changeset [695] by campbell
Rearrange Clight files a bit - will try to make them work again soon…
12:30 PM Changeset [694] by campbell
Start moving Clight into common directory.
12:11 PM Changeset [693] by campbell
Separate out whole program executions from the clight semantics and …
11:36 AM Changeset [692] by mulligan
Deleted files.
11:36 AM Changeset [691] by mulligan
More movement of files within the repository.
11:34 AM Changeset [690] by mulligan
Moved new matita files into correct place.
11:33 AM Changeset [689] by mulligan
Got rid of old Matita development files.
11:31 AM Changeset [688] by mulligan
Fixed local conflicts. Restructured svn repository.
11:23 AM Changeset [687] by mulligan
Renamed to enforce consistency of filenames
11:22 AM Changeset [686] by mulligan
Most of LIN completed.

Mar 16, 2011:

2:36 PM Changeset [685] by ayache
Bug fix in LINToASM (wrong conditional translation) in 8051 branch.
10:14 AM Changeset [684] by sacerdot
Moved into Presentations.

Mar 15, 2011:

2:47 PM Changeset [683] by mulligan
Changes from working on my PC.
2:22 PM Changeset [682] by sacerdot
2:20 PM Changeset [681] by sacerdot
2:19 PM Changeset [680] by sacerdot
8051-memoryspace-branch from Brian moved from D2.3 (that does not …
2:13 PM Changeset [679] by sacerdot
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 Ian Stark
(diff)
9:10 AM Changeset [678] by amadio
WP-rob update
9:05 AM Changeset [677] by campbell
Use better titles for T3.2/3.3.

Mar 10, 2011:

5:46 PM Changeset [676] by sacerdot
4:26 PM Changeset [675] by sacerdot
4:19 PM Changeset [674] by sacerdot
4:10 PM Changeset [673] by regisgia
* Cosmetics.
3:16 PM Changeset [672] by regisgia
* Slides shuffling.
2:56 PM Changeset [671] by mulligan
Finished demo script for tomorrow.
2:50 PM Changeset [670] by regisgia
* New version of the video.
2:14 PM Changeset [669] by mulligan
Fixed man months
1:46 PM Changeset [668] by mulligan
small changes
1:45 PM Changeset [667] by mulligan
Changes to presentation that claudio wanted
1:20 PM Changeset [666] by amadio
WP-roberto update
11:52 AM Changeset [665] by sacerdot
11:48 AM Changeset [664] by mulligan
Changed output of Intel HEX files so we no longer have those …
9:43 AM Changeset [663] by regisgia
* Video of prototype demonstration.
9:39 AM Changeset [662] by regisgia
New version of the slides.
Note: See TracTimeline for information about the timeline view.