chiark / gitweb /
Ian Jackson [Mon, 12 Mar 2012 15:50:59 +0000 (15:50 +0000)]
formatting: section headings on lh pages too
Ian Jackson [Mon, 12 Mar 2012 15:36:53 +0000 (15:36 +0000)]
in simple commit rename parent from A to L
Ian Jackson [Mon, 12 Mar 2012 15:35:30 +0000 (15:35 +0000)]
add purported proof of calculation of ends
Ian Jackson [Mon, 12 Mar 2012 15:34:45 +0000 (15:34 +0000)]
fix calculation of ends formula
Ian Jackson [Mon, 12 Mar 2012 15:17:46 +0000 (15:17 +0000)]
assert that exact ancestors is trivial
Ian Jackson [Mon, 12 Mar 2012 15:15:51 +0000 (15:15 +0000)]
proof of alternative merge formulation
Ian Jackson [Mon, 12 Mar 2012 15:15:37 +0000 (15:15 +0000)]
remove trailing ws
Ian Jackson [Mon, 12 Mar 2012 14:52:51 +0000 (14:52 +0000)]
create tip
Ian Jackson [Mon, 12 Mar 2012 14:51:27 +0000 (14:51 +0000)]
simple commit foreign inclusion use simple foreign inclusion
Ian Jackson [Mon, 12 Mar 2012 14:48:50 +0000 (14:48 +0000)]
introduce and use Totally Foreign Contents
Ian Jackson [Mon, 12 Mar 2012 14:38:24 +0000 (14:38 +0000)]
wip create tip
Ian Jackson [Mon, 12 Mar 2012 14:37:47 +0000 (14:37 +0000)]
add missing []
Ian Jackson [Mon, 12 Mar 2012 14:37:37 +0000 (14:37 +0000)]
improve proof of create base inclusion
Ian Jackson [Mon, 12 Mar 2012 14:29:08 +0000 (14:29 +0000)]
create tip wip
Ian Jackson [Mon, 12 Mar 2012 14:28:13 +0000 (14:28 +0000)]
introduce macros \pq \pqy \pqn
Ian Jackson [Mon, 12 Mar 2012 14:18:49 +0000 (14:18 +0000)]
create base rename cond to create acyclic
Ian Jackson [Mon, 12 Mar 2012 14:17:50 +0000 (14:17 +0000)]
create base fix base acyclic and condition
Ian Jackson [Mon, 12 Mar 2012 14:13:49 +0000 (14:13 +0000)]
wip create tip
Ian Jackson [Mon, 12 Mar 2012 14:13:20 +0000 (14:13 +0000)]
todo list item
Ian Jackson [Mon, 12 Mar 2012 14:12:52 +0000 (14:12 +0000)]
use Q not B as patch name in create base
Ian Jackson [Mon, 12 Mar 2012 13:57:55 +0000 (13:57 +0000)]
rename Ingredients Prohibit Replay to Prevent
Ian Jackson [Mon, 12 Mar 2012 13:57:35 +0000 (13:57 +0000)]
replace various no replay with Ingredients Prohibit Replay
Ian Jackson [Mon, 12 Mar 2012 13:56:55 +0000 (13:56 +0000)]
rename merge Ordering of L... to Ordering of Ingredients
Ian Jackson [Mon, 12 Mar 2012 13:40:27 +0000 (13:40 +0000)]
create base foreign contents
Ian Jackson [Mon, 12 Mar 2012 13:40:19 +0000 (13:40 +0000)]
change Not Applicable [] to Not Applicable
Ian Jackson [Mon, 12 Mar 2012 13:39:14 +0000 (13:39 +0000)]
create base foreign inclusion
Ian Jackson [Mon, 12 Mar 2012 08:55:53 +0000 (08:55 +0000)]
wip create base
Ian Jackson [Sun, 11 Mar 2012 17:56:49 +0000 (17:56 +0000)]
create base coherence fix title
Ian Jackson [Sun, 11 Mar 2012 17:56:28 +0000 (17:56 +0000)]
create base fix def
Ian Jackson [Sun, 11 Mar 2012 17:43:32 +0000 (17:43 +0000)]
prove and use totally foreign contents
Ian Jackson [Sun, 11 Mar 2012 17:36:15 +0000 (17:36 +0000)]
fix some headings
Ian Jackson [Sun, 11 Mar 2012 17:35:27 +0000 (17:35 +0000)]
formalise foreign merges
Ian Jackson [Sun, 11 Mar 2012 17:35:13 +0000 (17:35 +0000)]
Foreign Contents section in a couple of places
Ian Jackson [Sun, 11 Mar 2012 17:34:15 +0000 (17:34 +0000)]
new foreign contents restriction
Ian Jackson [Sun, 11 Mar 2012 16:31:18 +0000 (16:31 +0000)]
fix a section => subsection
Ian Jackson [Sun, 11 Mar 2012 16:31:09 +0000 (16:31 +0000)]
fix create tip tbd
Ian Jackson [Sun, 11 Mar 2012 16:30:59 +0000 (16:30 +0000)]
wip create base
Ian Jackson [Sun, 11 Mar 2012 16:09:36 +0000 (16:09 +0000)]
merge conditions into conditions
Ian Jackson [Sun, 11 Mar 2012 16:09:27 +0000 (16:09 +0000)]
anticommit clarify note re ingredient order
Ian Jackson [Sun, 11 Mar 2012 16:09:14 +0000 (16:09 +0000)]
anticommit conditions into conditions
Ian Jackson [Sun, 11 Mar 2012 15:57:25 +0000 (15:57 +0000)]
wip creates
Ian Jackson [Sun, 11 Mar 2012 15:56:43 +0000 (15:56 +0000)]
formatting move/add some qeds
Ian Jackson [Sun, 11 Mar 2012 15:52:47 +0000 (15:52 +0000)]
simple commit unique base clarification
Ian Jackson [Sun, 11 Mar 2012 15:51:52 +0000 (15:51 +0000)]
annotation calculation
Ian Jackson [Sun, 11 Mar 2012 14:21:01 +0000 (14:21 +0000)]
fix up some lemmas re ends
Ian Jackson [Sun, 11 Mar 2012 14:07:39 +0000 (14:07 +0000)]
a todo item
Ian Jackson [Sun, 11 Mar 2012 14:05:33 +0000 (14:05 +0000)]
anticommit foreign inclusion
Ian Jackson [Sun, 11 Mar 2012 13:10:57 +0000 (13:10 +0000)]
a todo item
Ian Jackson [Sun, 11 Mar 2012 12:44:56 +0000 (12:44 +0000)]
wip anticommit foreign inclusion
Ian Jackson [Sun, 11 Mar 2012 12:35:23 +0000 (12:35 +0000)]
merge reference to no replay fix ref to be more regular
Ian Jackson [Sun, 11 Mar 2012 12:34:59 +0000 (12:34 +0000)]
anticommit make note re merge base vs merge rhs ordering
Ian Jackson [Sun, 11 Mar 2012 12:31:53 +0000 (12:31 +0000)]
anticommit - split out ordering
Ian Jackson [Sun, 11 Mar 2012 12:24:03 +0000 (12:24 +0000)]
merge coherence use two implies in statement since equiv cannot represent haspatch and nothaspatch
Ian Jackson [Sun, 11 Mar 2012 12:23:37 +0000 (12:23 +0000)]
anticommit coherence
Ian Jackson [Sun, 11 Mar 2012 12:08:10 +0000 (12:08 +0000)]
anticommit rename From Base to Into Base
Ian Jackson [Sun, 11 Mar 2012 12:07:19 +0000 (12:07 +0000)]
anticommit base acyclic
Ian Jackson [Sun, 11 Mar 2012 12:06:57 +0000 (12:06 +0000)]
strengthen anticommit condition to From Base
Ian Jackson [Sun, 11 Mar 2012 11:51:01 +0000 (11:51 +0000)]
merge foreign inclusion
Ian Jackson [Sun, 11 Mar 2012 11:48:14 +0000 (11:48 +0000)]
move alternative formulation of merge results into lemmas
Ian Jackson [Sun, 11 Mar 2012 11:24:26 +0000 (11:24 +0000)]
Prove that plain git merges on non-tb branches are ok
Ian Jackson [Sun, 11 Mar 2012 11:23:59 +0000 (11:23 +0000)]
Mention that simple commit justification applies to tb export too
Ian Jackson [Sun, 11 Mar 2012 11:21:31 +0000 (11:21 +0000)]
clarify text re non-tb flattened re-inclusion
Ian Jackson [Sun, 11 Mar 2012 11:07:12 +0000 (11:07 +0000)]
merge wip
Ian Jackson [Sun, 11 Mar 2012 11:06:04 +0000 (11:06 +0000)]
merge tip contents done
Ian Jackson [Sun, 11 Mar 2012 11:05:24 +0000 (11:05 +0000)]
merge tip contentss: clarify arbitrariness of D
Ian Jackson [Sun, 11 Mar 2012 11:04:59 +0000 (11:04 +0000)]
capitalise a few names
Ian Jackson [Sun, 11 Mar 2012 10:32:28 +0000 (10:32 +0000)]
merge remove redundant element in condition
Ian Jackson [Sun, 11 Mar 2012 09:02:57 +0000 (09:02 +0000)]
wip merge tip contents
Ian Jackson [Sun, 11 Mar 2012 08:58:18 +0000 (08:58 +0000)]
some alternative formulations of \merge
Ian Jackson [Sun, 11 Mar 2012 08:57:55 +0000 (08:57 +0000)]
add definition of \nequiv. \not\equiv still does not work for some reason
Ian Jackson [Sun, 11 Mar 2012 08:32:59 +0000 (08:32 +0000)]
wip merge tip contents
Ian Jackson [Sun, 11 Mar 2012 08:17:50 +0000 (08:17 +0000)]
wip merge tip contents
Ian Jackson [Sun, 11 Mar 2012 08:12:49 +0000 (08:12 +0000)]
wip merge tip contents
Ian Jackson [Thu, 8 Mar 2012 18:46:34 +0000 (18:46 +0000)]
wip merge tip contents
Ian Jackson [Thu, 8 Mar 2012 18:35:43 +0000 (18:35 +0000)]
wip merge tip contents
Ian Jackson [Thu, 8 Mar 2012 18:35:32 +0000 (18:35 +0000)]
merge base acyclic (and condition)
Ian Jackson [Thu, 8 Mar 2012 18:35:07 +0000 (18:35 +0000)]
clarify P sets none overlap
Ian Jackson [Thu, 8 Mar 2012 17:27:25 +0000 (17:27 +0000)]
wip merge tip contents
Ian Jackson [Thu, 8 Mar 2012 17:27:16 +0000 (17:27 +0000)]
rename exclusive tip contents corollary
Ian Jackson [Thu, 8 Mar 2012 17:06:18 +0000 (17:06 +0000)]
merge complex done
Ian Jackson [Thu, 8 Mar 2012 17:05:09 +0000 (17:05 +0000)]
wip merge complex - reformulate merge ends conditions
Ian Jackson [Thu, 8 Mar 2012 16:56:57 +0000 (16:56 +0000)]
merge ends condition - change condition to one that is equivalent but looks stronger and is easier to compute
Ian Jackson [Thu, 8 Mar 2012 16:50:41 +0000 (16:50 +0000)]
wip merge complex - final case?
Ian Jackson [Thu, 8 Mar 2012 16:40:16 +0000 (16:40 +0000)]
wip merge complex - fix bug, improve merge ends condition
Ian Jackson [Thu, 8 Mar 2012 16:21:33 +0000 (16:21 +0000)]
wip merge complex - a bug
Ian Jackson [Thu, 8 Mar 2012 16:21:23 +0000 (16:21 +0000)]
wip merge complex
Ian Jackson [Thu, 8 Mar 2012 16:20:50 +0000 (16:20 +0000)]
improve merge ends formatting
Ian Jackson [Thu, 8 Mar 2012 15:25:27 +0000 (15:25 +0000)]
wip merge complex - C = D
Ian Jackson [Thu, 8 Mar 2012 15:24:45 +0000 (15:24 +0000)]
wip merge complex - a fix
Ian Jackson [Tue, 6 Mar 2012 21:16:55 +0000 (21:16 +0000)]
wip merge complex
Ian Jackson [Tue, 6 Mar 2012 17:47:49 +0000 (17:47 +0000)]
wip merge complex
Ian Jackson [Tue, 6 Mar 2012 17:46:30 +0000 (17:46 +0000)]
use \p rather than just P
Ian Jackson [Tue, 6 Mar 2012 17:31:13 +0000 (17:31 +0000)]
wip merge complex
Ian Jackson [Tue, 6 Mar 2012 17:29:22 +0000 (17:29 +0000)]
move merge X and Y def up
Ian Jackson [Tue, 6 Mar 2012 17:17:07 +0000 (17:17 +0000)]
tiny clarification
Ian Jackson [Tue, 6 Mar 2012 17:16:58 +0000 (17:16 +0000)]
introduce \proofstarts
Ian Jackson [Tue, 6 Mar 2012 17:11:17 +0000 (17:11 +0000)]
wip merge content
Ian Jackson [Tue, 6 Mar 2012 14:41:54 +0000 (14:41 +0000)]
add some xxx's
Ian Jackson [Tue, 6 Mar 2012 14:34:10 +0000 (14:34 +0000)]
anticommit desired contents
Ian Jackson [Tue, 6 Mar 2012 14:33:33 +0000 (14:33 +0000)]
Rename \merge to \mergeof so we can have \merge