chiark / gitweb /
topbloke-formulae.git
7 years agowip dependency insertion
Ian Jackson [Wed, 14 Mar 2012 18:27:25 +0000 (18:27 +0000)]
wip dependency insertion

7 years agorename anticommit section
Ian Jackson [Wed, 14 Mar 2012 18:20:13 +0000 (18:20 +0000)]
rename anticommit section

7 years agomore clarifications and fixes from reread
Ian Jackson [Mon, 12 Mar 2012 18:04:51 +0000 (18:04 +0000)]
more clarifications and fixes from reread

7 years agomore clarifications and fixes from reread
Ian Jackson [Mon, 12 Mar 2012 17:59:57 +0000 (17:59 +0000)]
more clarifications and fixes from reread

7 years agomore clarifications and fixes from reread
Ian Jackson [Mon, 12 Mar 2012 17:59:28 +0000 (17:59 +0000)]
more clarifications and fixes from reread

7 years agoclarifications and fixes from reread
Ian Jackson [Mon, 12 Mar 2012 17:02:50 +0000 (17:02 +0000)]
clarifications and fixes from reread

7 years agoimprove wording
Ian Jackson [Mon, 12 Mar 2012 16:11:41 +0000 (16:11 +0000)]
improve wording

7 years agoimprove wording
Ian Jackson [Mon, 12 Mar 2012 16:09:29 +0000 (16:09 +0000)]
improve wording

7 years agocreate base: remove ingredients condition
Ian Jackson [Mon, 12 Mar 2012 16:06:18 +0000 (16:06 +0000)]
create base: remove ingredients condition

7 years agocreate base: strengthen create acyclic condition
Ian Jackson [Mon, 12 Mar 2012 16:03:36 +0000 (16:03 +0000)]
create base: strengthen create acyclic condition

7 years agoformatting: a couple of extra [ ]
Ian Jackson [Mon, 12 Mar 2012 15:53:40 +0000 (15:53 +0000)]
formatting: a couple of extra [ ]

7 years agoformatting: section headings on lh pages too
Ian Jackson [Mon, 12 Mar 2012 15:50:59 +0000 (15:50 +0000)]
formatting: section headings on lh pages too

7 years agoin simple commit rename parent from A to L
Ian Jackson [Mon, 12 Mar 2012 15:36:53 +0000 (15:36 +0000)]
in simple commit rename parent from A to L

7 years agoadd purported proof of calculation of ends
Ian Jackson [Mon, 12 Mar 2012 15:35:30 +0000 (15:35 +0000)]
add purported proof of calculation of ends

7 years agofix calculation of ends formula
Ian Jackson [Mon, 12 Mar 2012 15:34:45 +0000 (15:34 +0000)]
fix calculation of ends formula

7 years agoassert that exact ancestors is trivial
Ian Jackson [Mon, 12 Mar 2012 15:17:46 +0000 (15:17 +0000)]
assert that exact ancestors is trivial

7 years agoproof of alternative merge formulation
Ian Jackson [Mon, 12 Mar 2012 15:15:51 +0000 (15:15 +0000)]
proof of alternative merge formulation

7 years agoremove trailing ws
Ian Jackson [Mon, 12 Mar 2012 15:15:37 +0000 (15:15 +0000)]
remove trailing ws

7 years agocreate tip
Ian Jackson [Mon, 12 Mar 2012 14:52:51 +0000 (14:52 +0000)]
create tip

7 years agosimple commit foreign inclusion use simple foreign inclusion
Ian Jackson [Mon, 12 Mar 2012 14:51:27 +0000 (14:51 +0000)]
simple commit foreign inclusion use simple foreign inclusion

7 years agointroduce and use Totally Foreign Contents
Ian Jackson [Mon, 12 Mar 2012 14:48:50 +0000 (14:48 +0000)]
introduce and use Totally Foreign Contents

7 years agowip create tip
Ian Jackson [Mon, 12 Mar 2012 14:38:24 +0000 (14:38 +0000)]
wip create tip

7 years agoadd missing []
Ian Jackson [Mon, 12 Mar 2012 14:37:47 +0000 (14:37 +0000)]
add missing []

7 years agoimprove proof of create base inclusion
Ian Jackson [Mon, 12 Mar 2012 14:37:37 +0000 (14:37 +0000)]
improve proof of create base inclusion

7 years agocreate tip wip
Ian Jackson [Mon, 12 Mar 2012 14:29:08 +0000 (14:29 +0000)]
create tip wip

7 years agointroduce macros \pq \pqy \pqn
Ian Jackson [Mon, 12 Mar 2012 14:28:13 +0000 (14:28 +0000)]
introduce macros \pq \pqy \pqn

7 years agocreate base rename cond to create acyclic
Ian Jackson [Mon, 12 Mar 2012 14:18:49 +0000 (14:18 +0000)]
create base rename cond to create acyclic

7 years agocreate base fix base acyclic and condition
Ian Jackson [Mon, 12 Mar 2012 14:17:50 +0000 (14:17 +0000)]
create base fix base acyclic and condition

7 years agowip create tip
Ian Jackson [Mon, 12 Mar 2012 14:13:49 +0000 (14:13 +0000)]
wip create tip

7 years agotodo list item
Ian Jackson [Mon, 12 Mar 2012 14:13:20 +0000 (14:13 +0000)]
todo list item

7 years agouse Q not B as patch name in create base
Ian Jackson [Mon, 12 Mar 2012 14:12:52 +0000 (14:12 +0000)]
use Q not B as patch name in create base

7 years agorename Ingredients Prohibit Replay to Prevent
Ian Jackson [Mon, 12 Mar 2012 13:57:55 +0000 (13:57 +0000)]
rename Ingredients Prohibit Replay to Prevent

7 years agoreplace various no replay with Ingredients Prohibit Replay
Ian Jackson [Mon, 12 Mar 2012 13:57:35 +0000 (13:57 +0000)]
replace various no replay with Ingredients Prohibit Replay

7 years agorename merge Ordering of L... to Ordering of Ingredients
Ian Jackson [Mon, 12 Mar 2012 13:56:55 +0000 (13:56 +0000)]
rename merge Ordering of L... to Ordering of Ingredients

7 years agocreate base foreign contents
Ian Jackson [Mon, 12 Mar 2012 13:40:27 +0000 (13:40 +0000)]
create base foreign contents

7 years agochange Not Applicable [] to Not Applicable
Ian Jackson [Mon, 12 Mar 2012 13:40:19 +0000 (13:40 +0000)]
change Not Applicable [] to Not Applicable

7 years agocreate base foreign inclusion
Ian Jackson [Mon, 12 Mar 2012 13:39:14 +0000 (13:39 +0000)]
create base foreign inclusion

7 years agowip create base
Ian Jackson [Mon, 12 Mar 2012 08:55:53 +0000 (08:55 +0000)]
wip create base

7 years agocreate base coherence fix title
Ian Jackson [Sun, 11 Mar 2012 17:56:49 +0000 (17:56 +0000)]
create base coherence fix title

7 years agocreate base fix def
Ian Jackson [Sun, 11 Mar 2012 17:56:28 +0000 (17:56 +0000)]
create base fix def

7 years agoprove and use totally foreign contents
Ian Jackson [Sun, 11 Mar 2012 17:43:32 +0000 (17:43 +0000)]
prove and use totally foreign contents

7 years agofix some headings
Ian Jackson [Sun, 11 Mar 2012 17:36:15 +0000 (17:36 +0000)]
fix some headings

7 years agoformalise foreign merges
Ian Jackson [Sun, 11 Mar 2012 17:35:27 +0000 (17:35 +0000)]
formalise foreign merges

7 years agoForeign Contents section in a couple of places
Ian Jackson [Sun, 11 Mar 2012 17:35:13 +0000 (17:35 +0000)]
Foreign Contents section in a couple of places

7 years agonew foreign contents restriction
Ian Jackson [Sun, 11 Mar 2012 17:34:15 +0000 (17:34 +0000)]
new foreign contents restriction

7 years agofix a section => subsection
Ian Jackson [Sun, 11 Mar 2012 16:31:18 +0000 (16:31 +0000)]
fix a section => subsection

7 years agofix create tip tbd
Ian Jackson [Sun, 11 Mar 2012 16:31:09 +0000 (16:31 +0000)]
fix create tip tbd

7 years agowip create base
Ian Jackson [Sun, 11 Mar 2012 16:30:59 +0000 (16:30 +0000)]
wip create base

7 years agomerge conditions into conditions
Ian Jackson [Sun, 11 Mar 2012 16:09:36 +0000 (16:09 +0000)]
merge conditions into conditions

7 years agoanticommit clarify note re ingredient order
Ian Jackson [Sun, 11 Mar 2012 16:09:27 +0000 (16:09 +0000)]
anticommit clarify note re ingredient order

7 years agoanticommit conditions into conditions
Ian Jackson [Sun, 11 Mar 2012 16:09:14 +0000 (16:09 +0000)]
anticommit conditions into conditions

7 years agowip creates
Ian Jackson [Sun, 11 Mar 2012 15:57:25 +0000 (15:57 +0000)]
wip creates

7 years agoformatting move/add some qeds
Ian Jackson [Sun, 11 Mar 2012 15:56:43 +0000 (15:56 +0000)]
formatting move/add some qeds

7 years agosimple commit unique base clarification
Ian Jackson [Sun, 11 Mar 2012 15:52:47 +0000 (15:52 +0000)]
simple commit unique base clarification

7 years agoannotation calculation
Ian Jackson [Sun, 11 Mar 2012 15:51:52 +0000 (15:51 +0000)]
annotation calculation

7 years agofix up some lemmas re ends
Ian Jackson [Sun, 11 Mar 2012 14:21:01 +0000 (14:21 +0000)]
fix up some lemmas re ends

7 years agoa todo item
Ian Jackson [Sun, 11 Mar 2012 14:07:39 +0000 (14:07 +0000)]
a todo item

7 years agoanticommit foreign inclusion
Ian Jackson [Sun, 11 Mar 2012 14:05:33 +0000 (14:05 +0000)]
anticommit foreign inclusion

7 years agoa todo item
Ian Jackson [Sun, 11 Mar 2012 13:10:57 +0000 (13:10 +0000)]
a todo item

7 years agowip anticommit foreign inclusion
Ian Jackson [Sun, 11 Mar 2012 12:44:56 +0000 (12:44 +0000)]
wip anticommit foreign inclusion

7 years agomerge reference to no replay fix ref to be more regular
Ian Jackson [Sun, 11 Mar 2012 12:35:23 +0000 (12:35 +0000)]
merge reference to no replay fix ref to be more regular

7 years agoanticommit make note re merge base vs merge rhs ordering
Ian Jackson [Sun, 11 Mar 2012 12:34:59 +0000 (12:34 +0000)]
anticommit make note re merge base vs merge rhs ordering

7 years agoanticommit - split out ordering
Ian Jackson [Sun, 11 Mar 2012 12:31:53 +0000 (12:31 +0000)]
anticommit - split out ordering

7 years agomerge coherence use two implies in statement since equiv cannot represent haspatch...
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

7 years agoanticommit coherence
Ian Jackson [Sun, 11 Mar 2012 12:23:37 +0000 (12:23 +0000)]
anticommit coherence

7 years agoanticommit rename From Base to Into Base
Ian Jackson [Sun, 11 Mar 2012 12:08:10 +0000 (12:08 +0000)]
anticommit rename From Base to Into Base

7 years agoanticommit base acyclic
Ian Jackson [Sun, 11 Mar 2012 12:07:19 +0000 (12:07 +0000)]
anticommit base acyclic

7 years agostrengthen anticommit condition to From Base
Ian Jackson [Sun, 11 Mar 2012 12:06:57 +0000 (12:06 +0000)]
strengthen anticommit condition to From Base

7 years agomerge foreign inclusion
Ian Jackson [Sun, 11 Mar 2012 11:51:01 +0000 (11:51 +0000)]
merge foreign inclusion

7 years agomove alternative formulation of merge results into lemmas
Ian Jackson [Sun, 11 Mar 2012 11:48:14 +0000 (11:48 +0000)]
move alternative formulation of merge results into lemmas

7 years agoProve that plain git merges on non-tb branches are ok
Ian Jackson [Sun, 11 Mar 2012 11:24:26 +0000 (11:24 +0000)]
Prove that plain git merges on non-tb branches are ok

7 years agoMention that simple commit justification applies to tb export too
Ian Jackson [Sun, 11 Mar 2012 11:23:59 +0000 (11:23 +0000)]
Mention that simple commit justification applies to tb export too

7 years agoclarify text re non-tb flattened re-inclusion
Ian Jackson [Sun, 11 Mar 2012 11:21:31 +0000 (11:21 +0000)]
clarify text re non-tb flattened re-inclusion

7 years agomerge wip
Ian Jackson [Sun, 11 Mar 2012 11:07:12 +0000 (11:07 +0000)]
merge wip

7 years agomerge tip contents done
Ian Jackson [Sun, 11 Mar 2012 11:06:04 +0000 (11:06 +0000)]
merge tip contents done

7 years agomerge tip contentss: clarify arbitrariness of D
Ian Jackson [Sun, 11 Mar 2012 11:05:24 +0000 (11:05 +0000)]
merge tip contentss: clarify arbitrariness of D

7 years agocapitalise a few names
Ian Jackson [Sun, 11 Mar 2012 11:04:59 +0000 (11:04 +0000)]
capitalise a few names

7 years agomerge remove redundant element in condition
Ian Jackson [Sun, 11 Mar 2012 10:32:28 +0000 (10:32 +0000)]
merge remove redundant element in condition

7 years agowip merge tip contents
Ian Jackson [Sun, 11 Mar 2012 09:02:57 +0000 (09:02 +0000)]
wip merge tip contents

7 years agosome alternative formulations of \merge
Ian Jackson [Sun, 11 Mar 2012 08:58:18 +0000 (08:58 +0000)]
some alternative formulations of \merge

7 years agoadd definition of \nequiv. \not\equiv still does not work for some reason
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

7 years agowip merge tip contents
Ian Jackson [Sun, 11 Mar 2012 08:32:59 +0000 (08:32 +0000)]
wip merge tip contents

7 years agowip merge tip contents
Ian Jackson [Sun, 11 Mar 2012 08:17:50 +0000 (08:17 +0000)]
wip merge tip contents

7 years agowip merge tip contents
Ian Jackson [Sun, 11 Mar 2012 08:12:49 +0000 (08:12 +0000)]
wip merge tip contents

7 years agowip merge tip contents
Ian Jackson [Thu, 8 Mar 2012 18:46:34 +0000 (18:46 +0000)]
wip merge tip contents

7 years agowip merge tip contents
Ian Jackson [Thu, 8 Mar 2012 18:35:43 +0000 (18:35 +0000)]
wip merge tip contents

7 years agomerge base acyclic (and condition)
Ian Jackson [Thu, 8 Mar 2012 18:35:32 +0000 (18:35 +0000)]
merge base acyclic (and condition)

7 years agoclarify P sets none overlap
Ian Jackson [Thu, 8 Mar 2012 18:35:07 +0000 (18:35 +0000)]
clarify P sets none overlap

7 years agowip merge tip contents
Ian Jackson [Thu, 8 Mar 2012 17:27:25 +0000 (17:27 +0000)]
wip merge tip contents

7 years agorename exclusive tip contents corollary
Ian Jackson [Thu, 8 Mar 2012 17:27:16 +0000 (17:27 +0000)]
rename exclusive tip contents corollary

7 years agomerge complex done
Ian Jackson [Thu, 8 Mar 2012 17:06:18 +0000 (17:06 +0000)]
merge complex done

7 years agowip merge complex - reformulate merge ends conditions
Ian Jackson [Thu, 8 Mar 2012 17:05:09 +0000 (17:05 +0000)]
wip merge complex - reformulate merge ends conditions

7 years agomerge ends condition - change condition to one that is equivalent but looks stronger...
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

7 years agowip merge complex - final case?
Ian Jackson [Thu, 8 Mar 2012 16:50:41 +0000 (16:50 +0000)]
wip merge complex - final case?

7 years agowip merge complex - fix bug, improve merge ends condition
Ian Jackson [Thu, 8 Mar 2012 16:40:16 +0000 (16:40 +0000)]
wip merge complex - fix bug, improve merge ends condition

7 years agowip merge complex - a bug
Ian Jackson [Thu, 8 Mar 2012 16:21:33 +0000 (16:21 +0000)]
wip merge complex - a bug

7 years agowip merge complex
Ian Jackson [Thu, 8 Mar 2012 16:21:23 +0000 (16:21 +0000)]
wip merge complex

7 years agoimprove merge ends formatting
Ian Jackson [Thu, 8 Mar 2012 16:20:50 +0000 (16:20 +0000)]
improve merge ends formatting

7 years agowip merge complex - C = D
Ian Jackson [Thu, 8 Mar 2012 15:25:27 +0000 (15:25 +0000)]
wip merge complex - C = D

7 years agowip merge complex - a fix
Ian Jackson [Thu, 8 Mar 2012 15:24:45 +0000 (15:24 +0000)]
wip merge complex - a fix