Timeline
Oct 12, 2011:
- 9:11 PM Changeset [1363] by
- - done stuff with create_label_trie
- 5:54 PM Changeset [1362] by
- d4-2 report almost complete
- 11:52 AM Changeset [1361] by
- more changes
- 11:47 AM Changeset [1360] by
- added more on use of dependent types, and also discussing the …
Oct 11, 2011:
- 6:00 PM Changeset [1359] by
- 1. more work on the RTL semantics 2. changes to joint/semantics to …
- 5:48 PM Changeset [1358] by
- got rtlabs to rtl compiling, foldi_strong needs examining
- 5:42 PM Changeset [1357] by
- * changed implementation of constant indexings with extensible arrays …
- 5:33 PM Changeset [1356] by
- deleted redundant directory. added outlines for both reports, and …
- 3:32 PM Changeset [1355] by
- monadic fold_lefti added
- 2:38 PM Changeset [1354] by
- One axiom closed.
- 12:45 PM Changeset [1353] by
- This commit is made necessary by the last Matita change. Inclusion is …
- 12:45 PM Changeset [1352] by
- This commit is made necessary by the last Matita change. Inclusion is …
- 12:24 PM Changeset [1351] by
- Tidy up some loose ends from the invariants branch merge.
- 2:27 AM Changeset [1350] by
- Porting to latest destruct tactic. Note: the tactics has a few …
Oct 10, 2011:
- 11:32 PM Changeset [1349] by
- * work on LIN completed * small implementation of extensible arrays
- 10:40 PM Changeset [1348] by
- …
- 7:22 PM Changeset [1347] by
- Remove obsolete definitions.
- 6:18 PM Changeset [1346] by
- Minor corrections and a paragraph of context in the abstract to …
- 5:50 PM Changeset [1345] by
- work on ERTL and LTL completed
- 5:47 PM Changeset [1344] by
- Ported to new destruct.
- 5:27 PM Changeset [1343] by
- fixed some bugs in the translation
- 5:16 PM Changeset [1342] by
- The new auto is much more powerful.
- 4:38 PM Changeset [1341] by
- Empty directory removed.
- 4:34 PM Changeset [1340] by
- work on RTLabs and RTL completed
- 4:10 PM Changeset [1339] by
- Automation is now stronger.
- 4:05 PM Changeset [1338] by
- Automation is now stronger.
- 4:03 PM Changeset [1337] by
- Automation is now stronger.
- 3:54 PM Changeset [1336] by
- Ported to new Matita destruct/inversion. One lemma fails at qed. …
- 3:54 PM Changeset [1335] by
- Ported to new Matita stdlib.
- 2:17 PM Changeset [1334] by
- work on Cminor completed
- 12:53 PM Changeset [1333] by
- Avoid using the name of the construction of jmeq.
- 12:41 PM Changeset [1332] by
- Summation example updated (needs computational K).
- 10:21 AM Changeset [1331] by
- some changes, but i now have two contradictory proof obligations.
Oct 7, 2011:
- 6:39 PM Changeset [1330] by
- Evict obsolete file.
- 6:19 PM Changeset [1329] by
- 1. Definition of addresses moved to BEMem 2. Basic functions on …
- 5:47 PM Changeset [1328] by
- * bug in ClightUtilities?.find_max_depth_lbld fixed * single-entry loop …
- 4:15 PM Changeset [1327] by
- More progress in the implementation of the ERTL specific statements. …
- 3:48 PM Changeset [1326] by
- Code improved (now it uses the high level functions from …
- 3:45 PM Changeset [1325] by
- finished implementing the translate constant function
- 3:32 PM Changeset [1324] by
- The semantics of extended statements must also consider the label …
- 3:26 PM Changeset [1323] by
- Reduce number of notations for destructive let on pairs to one.
- 2:59 PM Changeset [1322] by
- address => stack_address
- 2:37 PM Changeset [1321] by
- No longer/never implemented files removed.
- 2:17 PM Changeset [1320] by
- Frame operations implemented.
- 1:48 PM Changeset [1319] by
- indexing branch is compiling again: * clight interpreter updated * …
- 1:48 PM Changeset [1318] by
- Frame management implemented.
- 12:28 PM Changeset [1317] by
- Fix listings in D3.2/D3.3.
- 12:26 PM Changeset [1316] by
- Merge in id-lookup-branch to trunk.
- 11:12 AM Changeset [1315] by
- another move for the same reason. got rtlabs > rtl compiling again by …
- 11:03 AM Changeset [1314] by
- name changes so that bash tab completion actually works with some …
Oct 6, 2011:
- 10:55 PM Changeset [1313] by
- (E)RTL semantics ported to new data type for save/pop frame (but not …
- 10:35 PM Changeset [1312] by
- Type of frame operations (pop_frame/save_frame) generalized to take in …
- 6:45 PM Changeset [1311] by
- Merge trunk to invariants branch, sorting out the handling of …
- 6:31 PM Changeset [1310] by
- * finished changes on annotator * implementing indexes in interpreter
- 6:09 PM Changeset [1309] by
- - refounded JEP
- 5:27 PM Changeset [1308] by
- changes to translate_cst
- 2:08 PM Changeset [1307] by
- adding translate_cst
- 11:19 AM Changeset [1306] by
- small changes to rtlabs. what axioms remain look hard to close. need …
- 11:07 AM Changeset [1305] by
- added indexes to loop constructors. Branch does not compile atm
- 1:24 AM Changeset [1304] by
- Work in progress.
- 12:16 AM Changeset [1303] by
- 1. LTL/semantics.ma added (work in progress) 2. init_locals fixed to …
Oct 5, 2011:
- 11:36 PM Changeset [1302] by
- ERTL/semantics.ma ported to joint/SemanticUtils (in progress)
- 11:35 PM Changeset [1301] by
- Axioms re-grouped according to their use.
- 10:43 PM Changeset [1300] by
- More (graph) axioms implemented. Look at the comments marked with XXX …
- 9:53 PM Changeset [1299] by
- Functions from RTL/semantics.ma generalized to work on every graph …
- 9:41 PM Changeset [1298] by
- - fetch_statement now takes in input the globalenv - fetch_statement …
- 6:04 PM Changeset [1297] by
- changed representation of indexings to a nameless one implemented with …
- 5:53 PM Changeset [1296] by
- changes
- 4:15 PM Changeset [1295] by
- More progress.
- 3:19 PM Changeset [1294] by
- RTL semantics: porting to joint semantics started.
- 2:47 PM Changeset [1293] by
- finished rtl abs to rtl transformation subject to closing some axioms …
- 11:15 AM Changeset [1292] by
- more added to rtlabs translation
- 10:20 AM Changeset [1291] by
- Started branch of untrusted compiler with indexed labels * added …
Oct 4, 2011:
- 2:00 AM Changeset [1290] by
- One more function ported to new Joint.
- 1:57 AM Changeset [1289] by
- semantics ported to latest Joint version
Oct 3, 2011:
- 5:33 PM Changeset [1288] by
- more added to rtlabs to rtl pass
- 4:55 PM Changeset [1287] by
- about 3/4 of the way through rtlabs to rtl now
- 4:07 PM Changeset [1286] by
- more changes to the rtl abs to rtl pass
- 3:08 PM Changeset [1285] by
- more implementation on maps, final push to get rtl abs to rtl working
- 8:35 AM Changeset [1284] by
- Bugs fixed: fresh_label changes the label universe, but this was not …
Sep 30, 2011:
- 3:12 AM Changeset [1283] by
- Bad programming practice removed: change_label is no longer required …
Sep 28, 2011:
- 11:50 PM Changeset [1282] by
- Cosmetic change: names of joint statements/instructions shortened and …
- 11:08 PM Changeset [1281] by
- Porting of all transformation to the joint syntax practically …
- 2:43 AM Changeset [1280] by
- Some progress in the porting of RTLAbstoRTL to the joint syntax: 1) …
- 2:41 AM Changeset [1279] by
- Bug fixed in definition of ltb.
Sep 27, 2011:
- 9:57 AM Changeset [1278] by
- oppargs requires two more arguments. RTLtoERTL to be fixed since it …
Sep 26, 2011:
- 6:58 PM Changeset [1277] by
- Runtime functions and conclusion for D3.2.
- 6:14 PM Changeset [1276] by
- Support for replacing operations with runtime support functions in …
- 6:07 PM Changeset [1275] by
- RTL ported to joint syntax, but: 1. bug discovered: opaccs should …
- 5:58 PM Changeset [1274] by
- starting removing axioms from adts and giving them proper implementations
- 5:57 PM Changeset [1273] by
- Remove generated file.
- 5:57 PM Changeset [1272] by
- Revert accidental commit.
- 4:24 PM Changeset [1271] by
- finished, kind of
- 3:59 PM Changeset [1270] by
- Making RTL syntax an instance of Joint.
- 3:06 PM Changeset [1269] by
- Useless include removed.
- 2:52 PM Changeset [1268] by
- 1) AST/Identifier.ma no longer used, utilities/IdentifierTools no …
- 12:41 PM Changeset [1267] by
- Other bits and pieces for D3.3.
- 12:09 PM Changeset [1266] by
- Added second projection.
- 11:29 AM Changeset [1265] by
- Revisions to D3.3.
Sep 23, 2011:
- 6:44 PM Changeset [1264] by
- Almost ported to new Joint syntax.
- 5:12 PM Changeset [1263] by
- changes
- 4:40 PM Changeset [1262] by
- RTLtoERTL ported to the joint syntax for ERTL. Now it is time to port …
- 4:17 PM Changeset [1261] by
- More of D3.2.
- 3:04 PM Changeset [1260] by
- commit for csc
- 11:49 AM Changeset [1259] by
- More progress towards new Joint data type.
- 1:47 AM Changeset [1258] by
- More progress towards porting to joint syntax.
Sep 22, 2011:
- 6:04 PM Changeset [1257] by
- More progress in porting to joint datatype.
- 6:03 PM Changeset [1256] by
- changes: added a mapi for graphs
- 4:23 PM Changeset [1255] by
- Major mistake fixed: op1 and op2 were assuming the source and dest …
- 4:16 PM Changeset [1254] by
- More progress towards porting of RTLtoERTL to joint syntax.
- 2:57 PM Changeset [1253] by
- uses.ma finished
- 2:49 PM Changeset [1252] by
- graph_params added to joint/Joint.ma, together with useful common …
- 2:29 PM Changeset [1251] by
- changes to get things compiling again after yet another CSC rearrangement!
- 12:02 PM Changeset [1250] by
- 1. Sigma types projections moved to utilities/extralib.ma 2. Extended …
- 11:41 AM Changeset [1249] by
- changes to get everything to typecheck again
- 10:13 AM Changeset [1248] by
- deleted files that do not compile in utilities, changed ertl.ma to use …
- 3:03 AM Changeset [1247] by
- Code (almost) ported to latest joint/Joint.ma datatype. I still need …
- 2:50 AM Changeset [1246] by
- Yet another change to Joint.ma to accomodate all passes. The concrete …
Sep 21, 2011:
- 10:22 PM Changeset [1245] by
- RTLtoERTL and LINToASM: porting to new Joint data type in progress. …
- 6:08 PM Changeset [1244] by
- Sort out Clight semantics equivalence proof for new SmallstepExec?.
- 5:53 PM Changeset [1243] by
- small changes
- 5:35 PM Changeset [1242] by
- Some clean-up.
- 5:28 PM Changeset [1241] by
- changes for claudio
- 5:24 PM Changeset [1240] by
- Ported to common definitions.
- 5:21 PM Changeset [1239] by
- RTLAbstoRTL ported to new datatypes. Note: RTL syntax/semantics is …
- 4:25 PM Changeset [1238] by
- Update Cminor and RTLabs to fit SmallstepExec? changes.
- 3:58 PM Changeset [1237] by
- Wrong commit repaired.
- 3:56 PM Changeset [1236] by
- LTLToLin.ma completed (up to a couple of daemons used to provide dead …
- 12:14 PM Changeset [1235] by
- Some basic material for D3.2, but not yet finished.
- 12:14 PM Changeset [1234] by
- Add (rather brief) draft of D3.3.
- 11:57 AM Changeset [1233] by
- 1) Ported to Brian's new dependent type for fullexec 2) Universe level …
- 11:24 AM Changeset [1232] by
- big changes: got what was implemented in the ertl to ltl pass type …
Sep 20, 2011:
- 7:11 PM Changeset [1231] by
- Change SmallstepExec? so that states can depend on global information. …
- 3:56 PM Changeset [1230] by
- more changes
- 1:26 PM Changeset [1229] by
- changes
Sep 19, 2011:
- 4:52 PM Changeset [1228] by
- some more changes
- 12:57 PM Changeset [1227] by
- changes
Sep 16, 2011:
- 7:16 PM Changeset [1226] by
- Adjust pretty printers for change in program records, try a test of each.
- 6:48 PM Changeset [1225] by
- Missing ; in proof
- 6:39 PM Changeset [1224] by
- Type of programs in common/AST made more dependent. In particular, the …
- 5:15 PM Changeset [1223] by
- changes
- 11:02 AM Changeset [1222] by
- LTL fully ported to the joint syntax.
- 10:53 AM Changeset [1221] by
- Cleanup.
Sep 15, 2011:
- 6:05 PM Changeset [1220] by
- ERTL ported to the new joint syntax.
- 5:40 PM Changeset [1219] by
- a little more added
- 4:56 PM Changeset [1218] by
- a lot added to interference graph calculation
- 4:42 PM Changeset [1217] by
- Only one axiom left.
- 3:33 PM Changeset [1216] by
- Update Clight semantics equivalence proof to match changes in …
- 3:04 PM Changeset [1215] by
- 1) Added shifting directly on pointers 2) More temporary axioms closed.
- 2:27 PM Changeset [1214] by
- res_to_opt function added to common/Errors and used in joint/semantics …
- 2:01 PM Changeset [1213] by
- 1) New values (joint/BEValues.ma) and memory model for the back-ends …
Sep 14, 2011:
- 5:03 PM Changeset [1212] by
- more added on interference graphs
- 4:14 PM Changeset [1211] by
- fixed interference file
- 4:04 PM Changeset [1210] by
- getting rid of typeclass-like records in favour of file-level axioms. …
Sep 13, 2011:
- 5:14 PM Changeset [1209] by
- more work on int. graphs
- 4:33 PM Changeset [1208] by
- added adts for sets, tables and priority sets in order to make life …
Sep 12, 2011:
- 4:20 PM Changeset [1207] by
- Second part of fixing temporaries in Clight to Cminor stage.
- 4:20 PM Changeset [1206] by
- First stage of fixing temporary generation in Clight/toCminor.ma.
Note: See TracTimeline
for information about the timeline view.
