[xiny] _ Defined subset, subStructure _which can be used for semigroup, monoid,_ Mon Sep 19 03:51:54 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-51-54-393741000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-51-54-393741000-PDT.html [xiny] Added itt_cyclic_group and removed itt_abelian_group for documentation._ Mon Sep 19 03:52:10 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-52-10-441026000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-52-10-441026000-PDT.html [xiny] _ Moved _csemigroup__the set of commutative semigroup_ and _cmonoid_ to_ Mon Sep 19 03:52:10 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-52-10-811427000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-52-10-811427000-PDT.html [xiny] I_ve moved _commutative_ to _itt_grouplikeobj_ and _itt_group_._ Mon Sep 19 03:52:18 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-52-18-147553000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-52-18-147553000-PDT.html [xiny] _ Redefined _csemigroup_, _cmonoid_, and _abelg_ following Alexei_s advice._ Mon Sep 19 03:52:20 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-52-20-209363000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-52-20-209363000-PDT.html [xiny] Can anyone take a look at the rule _/itt_group/subgroup_isect__ I can_t_ Mon Sep 19 03:52:29 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-52-29-234637000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-52-29-234637000-PDT.html [xiny] _ Added some properties and reduction rules of the group power operation._ Mon Sep 19 03:52:29 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-52-29-669439000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-52-29-669439000-PDT.html [xiny] _ Proved that for if there is a positive number x such that P[x], then there_ Mon Sep 19 03:52:34 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-52-34-427188000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-52-34-427188000-PDT.html [xiny] _ Added reduce resource for group_power__ Mon Sep 19 03:52:41 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-52-41-163814000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-52-41-163814000-PDT.html [xiny] _ First try of defining group homomorphism._ Mon Sep 19 03:52:51 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-52-51-118008000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-52-51-118008000-PDT.html [xiny] _ Proved some properties of group homomorphism._ Mon Sep 19 03:52:56 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-52-56-128336000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-52-56-128336000-PDT.html [nogin] Aleksey _ Xin__ Mon Sep 19 03:53:07 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-53-07-797642000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-53-07-797642000-PDT.html [nogin] Xin _ Aleksey__ Mon Sep 19 03:53:11 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-53-11-019395000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-53-11-019395000-PDT.html [nogin] _ Working on cleaning up and documenting the term addresses interfaces_ Mon Sep 19 03:53:26 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-53-26-462943000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-53-26-462943000-PDT.html [yegor] 1. itt_bool _ equivalence of _x_false in bool_ and _assert_not x__._ Mon Sep 19 03:53:27 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-53-27-545111000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-53-27-545111000-PDT.html [nogin] _ Messed with the line_buffer and overflow code to get it do actually produce_ Mon Sep 19 03:54:29 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-54-29-209053000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-54-29-209053000-PDT.html [xiny] _ Added intro/elim rules for all concepts in itt_grouplikeobj.ml and added_ Mon Sep 19 03:54:29 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-54-29-717528000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-54-29-717528000-PDT.html [kopylov] Partially fix an old bug with parser. Now you can write_ Mon Sep 19 03:54:51 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-54-51-958897000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-54-51-958897000-PDT.html [nogin] _ This is a _major change_ in how sequent contexts are now handles in rule_ Mon Sep 19 03:54:52 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-54-52-362890000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-54-52-362890000-PDT.html [kopylov] I simplify definition of the subset relation._ Mon Sep 19 03:55:37 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-55-37-484691000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-55-37-484691000-PDT.html [kopylov] 1. Fix broken proofs._ Mon Sep 19 03:55:46 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-55-46-650910000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-55-46-650910000-PDT.html [kopylov] More on display forms and documentation_ Mon Sep 19 03:56:17 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-56-17-700931000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-56-17-700931000-PDT.html [nogin] Updated the list of people so that all sys descr. authors are also listed here._ Mon Sep 19 03:56:18 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-56-18-428079000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-56-18-428079000-PDT.html [nogin] Small no_op change in Term_ds address interface _needed to simplify adding_ Mon Sep 19 03:56:18 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-56-18-954014000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-56-18-954014000-PDT.html [jyh] This is the IR for the new letrec._ Mon Sep 19 03:56:19 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-56-19-404663000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-56-19-404663000-PDT.html [kopylov] I commit my current status of definition of red_black trees._ Mon Sep 19 03:56:20 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-56-20-028387000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-56-20-028387000-PDT.html [kopylov] Added new theories in print.ml_ Mon Sep 19 03:56:22 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-56-22-050178000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-56-22-050178000-PDT.html [kopylov] 1. Now parser never generate singleton record, but only empty record._ Mon Sep 19 03:56:22 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-56-22-777213000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-56-22-777213000-PDT.html [nogin] Fixed some _hopefull all__ bugs where rewrite mechanism was looking _counting_ Mon Sep 19 03:56:23 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-56-23-419190000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-56-23-419190000-PDT.html [jyh] Updated CPS._ Mon Sep 19 03:56:24 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-56-24-217515000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-56-24-217515000-PDT.html [nogin] Finally all our proofs replay with TERMS_std__ Mon Sep 19 03:56:24 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-56-24-879901000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-56-24-879901000-PDT.html [jyh] Updated closure conversion/dead code elimination/inlining to use the_ Mon Sep 19 03:56:25 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-56-25-334832000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-56-25-334832000-PDT.html [nogin] _ The rewriter now correctly makes sure that the SO var args have_ Mon Sep 19 03:56:26 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-56-26-682553000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-56-26-682553000-PDT.html [jyh] Generate initial assembly for the M language._ Mon Sep 19 03:56:29 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-56-29-409211000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-56-29-409211000-PDT.html [nogin] _ I moved the sequent_related __addr functions from TermMan to TermAddr_ Mon Sep 19 03:56:30 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-56-30-766445000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-56-30-766445000-PDT.html [jyh] Changed instruction format to use string parameters, like this__ Mon Sep 19 03:56:33 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-56-33-992573000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-56-33-992573000-PDT.html [jyh] Added code to split a live range._ Mon Sep 19 03:56:35 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-56-35-044052000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-56-35-044052000-PDT.html [] This commit was manufactured by cvs2svn to create branch _lm_libmojave_._ Mon Sep 19 03:56:36 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-56-36-170795000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-56-36-170795000-PDT.html [xiny] Fixed a typo._ Mon Sep 19 03:56:52 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-56-52-884132000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-56-52-884132000-PDT.html [nogin] _ Finished the proofs _and cleaned up_ in ctt_markov_ Mon Sep 19 03:56:53 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-56-53-287137000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-56-53-287137000-PDT.html [nogin] Killed some unused code._ Mon Sep 19 03:57:09 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-57-09-565520000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-57-09-565520000-PDT.html [xiny] Changed some rule names for consistence._ Mon Sep 19 03:57:10 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-57-10-032597000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-57-10-032597000-PDT.html [jyh] This is a branch commit._ Mon Sep 19 03:57:16 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-57-16-056581000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-57-16-056581000-PDT.html [jyh] Added register allocator code. So far unused._ Mon Sep 19 03:57:16 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-57-16-542466000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-57-16-542466000-PDT.html [jyh] Added x86 backend description._ Mon Sep 19 03:57:18 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-57-18-793117000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-57-18-793117000-PDT.html [xiny] _ Fixed some broken proofs._ Mon Sep 19 03:57:20 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-57-20-082475000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-57-20-082475000-PDT.html [kopylov] Commited some proofs._ Mon Sep 19 03:57:37 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-57-37-250798000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-57-37-250798000-PDT.html [jyh] Added main call to register allocator._ Mon Sep 19 03:57:44 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-57-44-172274000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-57-44-172274000-PDT.html [nogin] Changed the srripts to include the module name in each _status_ line_ Mon Sep 19 03:57:45 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-57-45-091576000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-57-45-091576000-PDT.html [jyh] Register allocation runs and produces an assignment, but we_ Mon Sep 19 03:57:45 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-57-45-555956000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-57-45-555956000-PDT.html [jyh] The problem with alpha_equality was because some MOVs _must__ Mon Sep 19 03:57:47 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-57-47-135069000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-57-47-135069000-PDT.html [nogin] Proved couple of rules that used to be prim._ Mon Sep 19 03:57:50 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-57-50-903350000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-57-50-903350000-PDT.html [nogin] Added a set membership elimination rule._ Mon Sep 19 03:57:53 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-57-53-141825000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-57-53-141825000-PDT.html [] This commit was manufactured by cvs2svn to create tag_ Mon Sep 19 03:57:59 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-57-59-601231000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-57-59-601231000-PDT.html [nogin] ___ WARNING ____ Mon Sep 19 03:58:15 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-58-15-664635000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-03-58-15-664635000-PDT.html [nogin] Print a meaningful error message _as opposed to uncaught Not_found_ when_ Mon Sep 19 04:12:16 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-12-16-952371000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-12-16-952371000-PDT.html [nogin] Restored the TESTS_yes compile._ Mon Sep 19 04:12:18 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-12-18-401834000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-12-18-401834000-PDT.html [jyh] Tailcalls take a variable number of arguments._ Mon Sep 19 04:12:20 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-12-21-002215000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-12-21-002215000-PDT.html [jyh] Added memory reserve statements to control GC._ Mon Sep 19 04:12:25 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-12-25-439753000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-12-25-439753000-PDT.html [jyh] _ Register allocator now adheres to calling convention._ Mon Sep 19 04:12:28 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-12-28-071937000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-12-28-071937000-PDT.html [nogin] _ Be even more strict about the variable name clashes _now that hypSubstT_ Mon Sep 19 04:12:32 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-12-32-900397000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-12-32-900397000-PDT.html [yegor] Prove of int_div_rem is 80_ complete._ Mon Sep 19 04:12:37 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-12-37-389430000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-12-37-389430000-PDT.html [yegor] Forgot two important branches._ Mon Sep 19 04:12:47 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-12-47-822324000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-12-47-822324000-PDT.html [jyh] One very important thing I forgot in the last commit_ I converted_ Mon Sep 19 04:13:14 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-13-14-319522000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-13-14-319522000-PDT.html [jyh] We now generate code the assembles without errors._ Mon Sep 19 04:13:17 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-13-17-744078000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-13-17-744078000-PDT.html [nogin] Implemented Alexei_s suggestion for the meaning of negative seq. context_ Mon Sep 19 04:13:20 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-13-20-352785000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-13-20-352785000-PDT.html [jyh] _ Yes_ Our first working program is fib_ It is just about as fast_ Mon Sep 19 04:13:23 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-13-23-141834000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-13-23-141834000-PDT.html [granicz] Updated the M parser to use records for functions._ Mon Sep 19 04:13:24 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-13-24-384336000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-13-24-384336000-PDT.html [nogin] ___ WARNING ____ Mon Sep 19 04:13:25 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-13-25-664793000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-13-25-664793000-PDT.html [nogin] Got rid of the signature files that were only used once._ Mon Sep 19 04:13:59 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-13-59-851851000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-13-59-851851000-PDT.html [yegor] In process of completing itt_nat/int_div_rem and debugging the arith tactic._ Mon Sep 19 04:14:00 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-00-904876000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-00-904876000-PDT.html [emre] Some typo fixes to documentation. _I_m tempted to go through and_ Mon Sep 19 04:14:12 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-12-769534000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-12-769534000-PDT.html [yegor] _subgoals_ debug variable added._ Mon Sep 19 04:14:14 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-14-579902000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-14-579902000-PDT.html [nogin] Enforce the type distinctions in Ascii_io _it used to be unnecessary,_ Mon Sep 19 04:14:15 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-15-045826000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-15-045826000-PDT.html [nogin] eflush should be passed via _t, no need to call it on a separate line._ Mon Sep 19 04:14:15 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-15-509538000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-15-509538000-PDT.html [jyh] _ Whew_ Fixed the register allocator, and completely rewrote the spill code._ Mon Sep 19 04:14:15 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-15-979147000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-15-979147000-PDT.html [yegor] Minor modifications of debug and error reporting code according to Aleksey_s_ Mon Sep 19 04:14:19 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-19-800810000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-19-800810000-PDT.html [nogin] Fixed a bug in alpha equality..._ Mon Sep 19 04:14:20 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-20-780288000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-20-780288000-PDT.html [emre] Killing the tab characters in the README file and adding my_ Mon Sep 19 04:14:22 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-22-793994000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-22-793994000-PDT.html [emre] I think CPS conversion is fine... fixing a typo in the section_ Mon Sep 19 04:14:23 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-23-315458000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-23-315458000-PDT.html [jyh] Starting the paper._ Mon Sep 19 04:14:24 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-24-535600000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-24-535600000-PDT.html [yegor] Aleksey _ Yegor__ Mon Sep 19 04:14:25 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-25-882723000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-25-882723000-PDT.html [jyh] Wrote something about the IR._ Mon Sep 19 04:14:32 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-32-823225000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-32-823225000-PDT.html [jyh] Added a section on CPS conversion._ Mon Sep 19 04:14:34 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-34-015098000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-34-015098000-PDT.html [jyh] Added a section on closure conversion._ Mon Sep 19 04:14:34 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-34-862133000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-34-862133000-PDT.html [emre] Thought a bit more about CPS conversion. I think I get what_s_ Mon Sep 19 04:14:35 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-35-593072000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-35-593072000-PDT.html [emre] Fixing an obvious mistake in the label/heading for the_ Mon Sep 19 04:14:36 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-36-052444000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-36-052444000-PDT.html [nogin] Make util _before_ libmojave _ this is the only way to make sure_ Mon Sep 19 04:14:37 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-37-214047000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-37-214047000-PDT.html [lolorigo] Updated the connection to the nuprl library to reflect nuprl_side changes. Jprover now connects directly to the nuprl refiner and uses a single connection instead of 2. The connection command is a comment at the top of editor/ml/nuprl_run.mli._ Mon Sep 19 04:14:37 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-37-683671000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-37-683671000-PDT.html [jyh] Added initial empty section on x86 asm._ Mon Sep 19 04:14:41 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-41-474012000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-41-474012000-PDT.html [jyh] Have to be a lot more aggressive about using _docoff to avoid_ Mon Sep 19 04:14:42 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-42-172362000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-42-172362000-PDT.html [jyh] Added a little moreon assembly._ Mon Sep 19 04:14:42 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-43-001446000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-43-001446000-PDT.html [granicz] Added a good chunk of the parsing section. I need to say something_ Mon Sep 19 04:14:43 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-43-514114000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-43-514114000-PDT.html [granicz] Added ACM templates. Changed the title of the paper to _Towards_ Mon Sep 19 04:14:46 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-46-683295000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-46-683295000-PDT.html [emre] Adding a few links at the end of the introduction. The main one_ Mon Sep 19 04:14:52 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-52-774499000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-52-774499000-PDT.html [jyh] Added a section on the assembly._ Mon Sep 19 04:14:54 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-54-592896000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-54-592896000-PDT.html [granicz] Cleaned out the main tex file._ Mon Sep 19 04:14:55 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-55-784976000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-55-784976000-PDT.html [nogin] Added a few comments and a few citations _note _ comments are agains the version_ Mon Sep 19 04:14:56 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-56-298479000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-56-298479000-PDT.html [jyh] Added a section on code generation._ Mon Sep 19 04:14:57 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-57-394944000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-57-394944000-PDT.html [granicz] Added currying to the parsing section._ Mon Sep 19 04:14:58 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-58-412970000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-58-412970000-PDT.html [jyh] Added a section on register allocation._ Mon Sep 19 04:14:59 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-59-711996000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-14-59-711996000-PDT.html [yegor] 1.Some bugs are fixed in polynomial normalization._ Mon Sep 19 04:15:01 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-01-206708000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-01-206708000-PDT.html [emre] Adding a comment at the end of the introduction about some_ Mon Sep 19 04:15:06 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-06-630695000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-06-630695000-PDT.html [emre] Adding another link to a paper _at the end of the introduction_._ Mon Sep 19 04:15:07 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-07-085520000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-07-085520000-PDT.html [jyh] Added some sections on optimization._ Mon Sep 19 04:15:07 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-07-803008000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-07-803008000-PDT.html [emre] Typo fixes only._ Mon Sep 19 04:15:08 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-08-704568000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-08-704568000-PDT.html [emre] I_m switching the paper to the alternate LaTeX style_ Mon Sep 19 04:15:09 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-09-847784000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-09-847784000-PDT.html [emre] A typo fix in x86_asm _bad label for the section_, and adding some_ Mon Sep 19 04:15:10 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-10-333968000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-10-333968000-PDT.html [emre] Adding some comments _mostly questions_ to the section on the IR._ Mon Sep 19 04:15:10 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-10-847412000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-10-847412000-PDT.html [jyh] Put the _thanks in the right place._ Mon Sep 19 04:15:11 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-11-344566000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-11-344566000-PDT.html [jyh] Files now pass the MetaPRL spell checker. Note, text in _comment___ Mon Sep 19 04:15:12 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-12-082536000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-12-082536000-PDT.html [nogin] Make sure it actually compiles with MP_DEBUG_spell. The problem was that the_ Mon Sep 19 04:15:14 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-14-662058000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-14-662058000-PDT.html [jyh] Revised the introduction._ Mon Sep 19 04:15:16 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-16-007916000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-16-007916000-PDT.html [granicz] Few typos and fixes._ Mon Sep 19 04:15:16 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-16-740363000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-16-740363000-PDT.html [jyh] Modified more of the introduction._ Mon Sep 19 04:15:17 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-17-371688000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-17-371688000-PDT.html [jyh] Modified the introduction._ Mon Sep 19 04:15:17 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-17-959486000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-17-959486000-PDT.html [emre] Inlining didn_t do anything for boolean values and conditions, so_ Mon Sep 19 04:15:18 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-18-453187000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-18-453187000-PDT.html [jyh] Modified the IR section._ Mon Sep 19 04:15:19 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-19-730107000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-19-730107000-PDT.html [granicz] Added some related work._ Mon Sep 19 04:15:21 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-21-563124000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-21-563124000-PDT.html [nogin] _ Make sure the system compiles with TESTS_yes _these fixes are already on_ Mon Sep 19 04:15:22 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-22-044481000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-22-044481000-PDT.html [nogin] A few comments._ Mon Sep 19 04:15:25 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-25-262864000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-25-262864000-PDT.html [jyh] Changes to the CPS section._ Mon Sep 19 04:15:26 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-26-729857000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-26-729857000-PDT.html [nogin] Another comment._ Mon Sep 19 04:15:27 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-27-447779000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-27-447779000-PDT.html [nogin] Wider comments._ Mon Sep 19 04:15:27 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-27-906711000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-27-906711000-PDT.html [emre] Deleting my comments in the Terminology section since they are no_ Mon Sep 19 04:15:28 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-28-381237000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-28-381237000-PDT.html [jyh] Modified closure conversion._ Mon Sep 19 04:15:29 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-29-690034000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-29-690034000-PDT.html [granicz] Added M syntax table and some fixes to the parsing text._ Mon Sep 19 04:15:30 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-30-855288000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-30-855288000-PDT.html [emre] Adding a response to one of Nogin_s comments in the introduction._ Mon Sep 19 04:15:31 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-31-478504000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-31-478504000-PDT.html [emre] Adding my comments on the current version of the parsing section._ Mon Sep 19 04:15:31 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-31-984054000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-31-984054000-PDT.html [granicz] Added a comment on naming intermediate values._ Mon Sep 19 04:15:32 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-32-533410000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-32-533410000-PDT.html [emre] My apologies if this conflicts with anyone else_s idea or work on_ Mon Sep 19 04:15:33 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-33-010357000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-33-010357000-PDT.html [jyh] I_m off to get intermittent sleep for the night._ Mon Sep 19 04:15:34 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-34-971626000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-34-971626000-PDT.html [nogin] Added a bunch of comments._ Mon Sep 19 04:15:35 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-35-920749000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-35-920749000-PDT.html [nogin] Typo._ Mon Sep 19 04:15:36 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-36-809569000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-36-809569000-PDT.html [nogin] Some thoughs on the conclusion. Or summary_ Is there a good distinction_ Mon Sep 19 04:15:37 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-37-381283000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-37-381283000-PDT.html [nogin] Started writing a brief cheat_list on semantics of compiler expressions._ Mon Sep 19 04:15:37 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-37-849909000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-37-849909000-PDT.html [yegor] Unintended change slipped into reduce_resource._ Mon Sep 19 04:15:39 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-39-940349000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-39-940349000-PDT.html [yegor] Sorry, didn_t want to change util/check_status._ Mon Sep 19 04:15:40 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-40-525555000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-40-525555000-PDT.html [emre] Minor typo fixes. Added inlining of branches in conditionals to_ Mon Sep 19 04:15:41 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-41-085354000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-41-085354000-PDT.html [emre] Perhaps a bit late to be coming up with this, but I think I_ Mon Sep 19 04:15:41 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-41-747928000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-41-747928000-PDT.html [emre] Killing the list of keywords, since we don_t strictly need them._ Mon Sep 19 04:15:43 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-43-441248000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-43-441248000-PDT.html [granicz] Added a couple comments to Brian_s._ Mon Sep 19 04:15:45 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-45-039796000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-45-039796000-PDT.html [granicz] Cut down the parsing section according to Jason_s comments._ Mon Sep 19 04:15:45 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-45-939027000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-45-939027000-PDT.html [nogin] check_status should indeed go to localhost._ Mon Sep 19 04:15:46 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-46-630339000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-46-630339000-PDT.html [granicz] A bit more precise description of what happens during parsing._ Mon Sep 19 04:15:47 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-47-317693000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-47-317693000-PDT.html [jyh] Added some terminology. Please comment._ Mon Sep 19 04:15:48 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-48-029705000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-48-029705000-PDT.html [nogin] MP_DEBUG_spell fixes._ Mon Sep 19 04:15:50 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-50-478883000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-50-478883000-PDT.html [nogin] New title._ Mon Sep 19 04:15:51 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-51-036040000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-51-036040000-PDT.html [xiny] Fixed the broken proof of positive_rule1._ Mon Sep 19 04:15:52 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-52-129830000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-52-129830000-PDT.html [jyh] Changed the intro._ Mon Sep 19 04:15:57 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-57-027589000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-57-027589000-PDT.html [emre] Fixing a display form so that the paper compiles._ Mon Sep 19 04:15:57 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-57-977905000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-57-977905000-PDT.html [emre] Addressing two of Justin_s minor comments that we didn_t get to_ Mon Sep 19 04:15:58 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-58-537493000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-58-537493000-PDT.html [nogin] Some rough text on FreshML._ Mon Sep 19 04:15:59 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-59-880970000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-15-59-880970000-PDT.html [emre] Added two citations for the IR _taken from a table in Appel_._ Mon Sep 19 04:16:02 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-02-103986000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-02-103986000-PDT.html [nogin] Another paper to cite._ Mon Sep 19 04:16:03 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-03-116409000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-03-116409000-PDT.html [nogin] Added another paragraph and citation to the related work section_ Mon Sep 19 04:16:03 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-03-706386000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-03-706386000-PDT.html [nogin] Added the Chaitin citation._ Mon Sep 19 04:16:04 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-04-554008000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-04-554008000-PDT.html [jyh] Added a summary section._ Mon Sep 19 04:16:05 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-05-326227000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-05-326227000-PDT.html [emre] Adding an alternate formulation of the paragraph on FreshML,_ Mon Sep 19 04:16:06 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-06-317764000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-06-317764000-PDT.html [nogin] Rewrote the FreshML par based on Brian_s version._ Mon Sep 19 04:16:07 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-07-340027000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-07-340027000-PDT.html [emre] Deleting Aleksey_s comment about the display forms for LetAtom and_ Mon Sep 19 04:16:07 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-07-864441000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-07-864441000-PDT.html [nogin] Typo._ Mon Sep 19 04:16:08 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-08-447975000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-08-447975000-PDT.html [jyh] Added an abstract._ Mon Sep 19 04:16:09 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-09-448881000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-09-448881000-PDT.html [emre] Another random comment on the summary. I_m having trouble finding_ Mon Sep 19 04:16:10 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-10-496189000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-10-496189000-PDT.html [granicz] Modified parsing section according to Jason_s comments._ Mon Sep 19 04:16:11 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-11-481733000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-11-481733000-PDT.html [nogin] Commented and uncommented in a few places._ Mon Sep 19 04:16:12 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-12-367248000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-12-367248000-PDT.html [emre] I have this paragraph that I want to write about work that has_ Mon Sep 19 04:16:13 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-13-133676000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-13-133676000-PDT.html [jyh] Various minor fixes._ Mon Sep 19 04:16:13 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-13-682336000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-13-682336000-PDT.html [nogin] Added a par on Liang_s Lambda_Prolog compiler. It seems to be _very__ Mon Sep 19 04:16:14 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-14-985964000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-14-985964000-PDT.html [emre] A typo fix to the abstract, and a comment on it _I must have_ Mon Sep 19 04:16:15 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-15-800406000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-15-800406000-PDT.html [granicz] Added heading for IR conversion section. I am working on the text._ Mon Sep 19 04:16:16 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-16-282764000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-16-282764000-PDT.html [nogin] The __fun__ rewrite in assembly generation still seems wrong._ Mon Sep 19 04:16:16 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-16-797767000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-16-797767000-PDT.html [jyh] Modified the parsing section._ Mon Sep 19 04:16:17 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-17-356359000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-17-356359000-PDT.html [nogin] YACC citation._ Mon Sep 19 04:16:20 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-20-144949000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-20-144949000-PDT.html [jyh] Updated the l_Prolog paragraph. Not sure it is so much better though._ Mon Sep 19 04:16:20 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-20-982163000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-20-982163000-PDT.html [granicz] Added section on AST_IR conversion. We are pushing the 12 page limit,_ Mon Sep 19 04:16:21 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-21-723862000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-21-723862000-PDT.html [granicz] Added citation for ASF_SDF and some text that mentions the_ Mon Sep 19 04:16:22 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-22-928377000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-22-928377000-PDT.html [emre] Adding a bib entry for the Mojave homepage. This I think resolves_ Mon Sep 19 04:16:25 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-25-575585000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-25-575585000-PDT.html [emre] More random fixes, comment clean_up. I_m going to give up for now_ Mon Sep 19 04:16:48 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-48-109187000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-48-109187000-PDT.html [emre] Still working on cleaning up the related work._ Mon Sep 19 04:16:53 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-53-638488000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-16-53-638488000-PDT.html [emre] A little blurb on typed assembly language that is not complete._ Mon Sep 19 04:17:00 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-17-00-374293000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-17-00-374293000-PDT.html [emre] Fixing more typos, and eliminating some redundant text._ Mon Sep 19 04:17:03 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-17-03-918244000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-17-03-918244000-PDT.html [jyh] Just rewrote Adam_s section on AST__IR._ Mon Sep 19 04:17:06 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-17-06-392581000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-17-06-392581000-PDT.html [emre] Removing the CVS conflict in the intro..._ Mon Sep 19 04:17:07 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-17-07-737039000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-17-07-737039000-PDT.html [emre] Fixing a bogus figure reference._ Mon Sep 19 04:17:08 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-17-08-520092000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-17-08-520092000-PDT.html [jyh] Moved related work to the end._ Mon Sep 19 04:17:09 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-17-09-570758000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-17-09-570758000-PDT.html [jyh] Minor updates in AST__IR._ Mon Sep 19 04:17:11 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-17-11-933423000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-17-11-933423000-PDT.html [jyh] Oops, I committed something that didn_t compile._ Mon Sep 19 04:17:12 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-17-12-997171000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-17-12-997171000-PDT.html [jyh] Almost_final version._ Mon Sep 19 04:17:13 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-17-13-989331000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-17-13-989331000-PDT.html [nogin] Final__ Mon Sep 19 04:17:15 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-17-15-523763000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-17-15-523763000-PDT.html [jyh] Forgot to commit deletion of HOAS._ Mon Sep 19 04:17:16 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-17-16-457009000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-17-16-457009000-PDT.html [] This commit was manufactured by cvs2svn to create tag_ Mon Sep 19 04:17:22 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-17-22-072512000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-17-22-072512000-PDT.html [nogin] Merged the lm_libmojave branch back to the trunk._ Mon Sep 19 04:17:37 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-17-37-161620000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-17-37-161620000-PDT.html [yegor] 1.Now arithT can deal with equality in conclusion _now it support lt,gt,le,ge,eq_. neq is still unsupported._ Mon Sep 19 04:17:52 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-17-52-243515000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-17-52-243515000-PDT.html [yegor] 1.Bugfix for previous commit _ equality _a_b in t_ in conclusion should be processed only if t is int and a is not b._ Mon Sep 19 04:19:01 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-19-01-317473000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-19-01-317473000-PDT.html [yegor] Oops, Makefile should not be changed _I don_t know how to fix it correctly_._ Mon Sep 19 04:19:04 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-19-04-742404000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-19-04-742404000-PDT.html [yegor] Small bugfix/optimization._ Mon Sep 19 04:19:05 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-19-05-379477000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-19-05-379477000-PDT.html [yegor] Small optimization _number of proof steps decreased but just a bit_._ Mon Sep 19 04:19:05 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-19-05-893170000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-19-05-893170000-PDT.html [nogin] Yegor, does this fix your PDIRS issues__ Mon Sep 19 04:19:06 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-19-06-676128000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-19-06-676128000-PDT.html [nogin] Fixed _make latex_._ Mon Sep 19 04:19:07 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-19-07-242294000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-19-07-242294000-PDT.html [nogin] _ New syntax for the documentation_ New syntax is_ Mon Sep 19 04:19:07 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-19-07-744408000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-19-07-744408000-PDT.html [nogin] MetaPRL now compiles with unmodified version of Ocaml 3.04._ Mon Sep 19 04:19:40 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-19-40-946794000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-19-40-946794000-PDT.html [yegor] 1.GPL header was missing in arith.ml, arith.mli_ Mon Sep 19 04:19:41 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-19-41-631416000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-19-41-631416000-PDT.html [nogin] Now MetaPRL requires ocaml 3.06 _get the RPMs at http_//rpm.nogin.org/ocaml.html_._ Mon Sep 19 04:21:27 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-21-27-536879000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-21-27-536879000-PDT.html [yegor] Support for nequal in conclusion added._ Mon Sep 19 04:21:31 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-21-31-798384000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-21-31-798384000-PDT.html [yegor] Working on support of negation in hyps._ Mon Sep 19 04:21:32 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-21-32-430818000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-21-32-430818000-PDT.html [yegor] Forgot to export proofs._ Mon Sep 19 04:21:33 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-21-33-069864000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-21-33-069864000-PDT.html [nogin] _ Proved all the rules in itt_record_exm_ Mon Sep 19 04:22:49 PDT 2005 http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-22-49-704470000-PDT.html http://svn.metaprl.org/commitlogs/metaprl/2003-03/2005-09-19-04-22-49-704470000-PDT.html