From 7821d152990aa729060705848c0a4b1051a14fb4 Mon Sep 17 00:00:00 2001 From: John Wiegley Date: Sat, 11 Oct 2014 22:01:46 -0500 Subject: [PATCH] coqPackages.domains: new expression --- .../coq-modules/coq-ext-lib/default.nix | 2 +- .../coq-modules/domains/darcs_context | 809 ++++++++++++++++++ .../coq-modules/domains/default.nix | 26 + pkgs/development/coq-modules/heq/default.nix | 2 +- pkgs/top-level/all-packages.nix | 2 + 5 files changed, 839 insertions(+), 2 deletions(-) create mode 100644 pkgs/development/coq-modules/domains/darcs_context create mode 100644 pkgs/development/coq-modules/domains/default.nix diff --git a/pkgs/development/coq-modules/coq-ext-lib/default.nix b/pkgs/development/coq-modules/coq-ext-lib/default.nix index 0d1b8bff954c..44173843033a 100644 --- a/pkgs/development/coq-modules/coq-ext-lib/default.nix +++ b/pkgs/development/coq-modules/coq-ext-lib/default.nix @@ -14,7 +14,7 @@ stdenv.mkDerivation rec { buildInputs = [ coq.ocaml coq.camlp5 ]; propagatedBuildInputs = [ coq ]; - installFlags = "COQLIB=$out/lib/coq/${coq.coq-version}"; + installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}"; meta = with stdenv.lib; { homepage = https://github.com/coq-ext-lib/coq-ext-lib; diff --git a/pkgs/development/coq-modules/domains/darcs_context b/pkgs/development/coq-modules/domains/darcs_context new file mode 100644 index 000000000000..5dac711c0c0a --- /dev/null +++ b/pkgs/development/coq-modules/domains/darcs_context @@ -0,0 +1,809 @@ + +Context: + +[additional facts about limits on cuts +robdockins@fastmail.fm**20140818025955 + Ignore-this: 6f9c952db425df6ae9d2a14139a8a3d1 +] + +[work on limits +robdockins@fastmail.fm**20140817221707 + Ignore-this: 9811e0cd669b48f3beb7a56d47cbe3c3 +] + +[finish proving that Q field ops commute with injq +robdockins@fastmail.fm**20140817060600 + Ignore-this: a1f6c62b39983e6f6f01d28aca5f8534 +] + +[split up realdom.v and perform associated code motion +robdockins@fastmail.fm**20140817030034 + Ignore-this: 24c74cd459d2ab15dcd3d83ba06f7081 +] + +[recip is canonical and converges +robdockins@fastmail.fm**20140725211947 + Ignore-this: c100dbd94114cca9576b2a3f46c9ddc7 +] + +[improve the proof that 1 is a unit for multiplication +robdockins@fastmail.fm**20140724150124 + Ignore-this: c5ec976f8a9858a7ba1f704b4e84d02e +] + +[complete proof the interval multiplication converges; other minor stuff +robdockins@fastmail.fm**20140724015132 + Ignore-this: bc717baa4c8f9ec31b821c5cfae5b499 +] + +[further progress in realdom.v +robdockins@fastmail.fm**20140723004023 + Ignore-this: f33e18d22ae69c9b6209e28151d18017 +] + +[unmessify rational_intervals patch +robdockins@fastmail.fm**20140721123718 + Ignore-this: 4a125b192a9964a508a1063845e9f160 +] + +[messy updates to rational_intervals.v +robdockins@fastmail.fm**20140721015810 + Ignore-this: 858dac9c55426167c6f397a71ef3fda5 +] + +[implicit arguments for "fixes" +robdockins@fastmail.fm**20140721015739 + Ignore-this: 229ecdd48265fc855319141e399bc522 +] + +[metadata +robdockins@fastmail.fm**20140714201441 + Ignore-this: aa16faaf09c1c404bdc6eaf0d0c39912 +] + +[further beautification +robdockins@fastmail.fm**20140714200516 + Ignore-this: 47d74c51d9fe130a5ac12706b1ddb1d4 +] + +[start working on the recripricol function +robdockins@fastmail.fm**20140714180055 + Ignore-this: c7f93cea17f46daa78a1ea14e86dfcaf +] + +[tweaks to the lambda models +robdockins@fastmail.fm**20140714180031 + Ignore-this: 219788fe70f42f0f6e60176cab464f19 +] + +[beauty edits in st_lam* +robdockins@fastmail.fm**20140714180006 + Ignore-this: a40aa7ae00ed27595ee04073918bd028 +] + +[move stuff to rational_intervals.v / define real_mult and prove some properties +robdockins@fastmail.fm**20140712053232 + Ignore-this: 398c5c03aac9ff37526d4d7c9e1a82c0 +] + +[finish correctness proof for interval multiplication +robdockins@fastmail.fm**20140711191547 + Ignore-this: c9ab138a0ca43fe0b133b208419bbcc4 +] + +[break out facts about rational intervals +robdockins@fastmail.fm**20140711012320 + Ignore-this: b7fe6e9377629a89b5debe3019ae1aa +] + +[updates to ideal completion +robdockins@fastmail.fm**20140707053800 + Ignore-this: 90d1efbd0e5833d8c83f0df056d7a74c +] + +[a pile of additional properties in realdom.v +robdockins@fastmail.fm**20140707053519 + Ignore-this: 7edba1e72a1856f297ef11e698ed989f +] + +[some properties of converging prereals +robdockins@fastmail.fm**20140706041401 + Ignore-this: 273bfbb245302becd7ff402831827ffb +] + +[make realdom compile +robdockins@fastmail.fm**20140630015439 + Ignore-this: 8bfc8eaeed4a1596450b0bb9ddef9aaa +] + +[renaming +robdockins@fastmail.fm**20140630011639 + Ignore-this: a287e083af095790cbf2b48df7a58739 +] + +[reorganize some code +robdockins@fastmail.fm**20140630011446 + Ignore-this: f1375b9e7ad822cb92f0c83d4001eddd +] + +[build the retract for realdom +robdockins@fastmail.fm**20140630001245 + Ignore-this: 4eb9da621588417d1b7b2fc980c7bf70 +] + +[fill out lemmas about cPLT +robdockins@fastmail.fm**20140630001140 + Ignore-this: add9e45c14621e3d6328684098bf8461 +] + +[more facts about cPLT +robdockins@fastmail.fm**20140628073731 + Ignore-this: 101a131ed114902924a1707eff7ebc70 +] + +[continuous domains as retracts of bifinite domains +robdockins@fastmail.fm**20140628035522 + Ignore-this: 5e7c61d49cf8424412b0d94f5fcb5ee6 +] + +[start implementing arithmetic operations in RealDom +robdockins@fastmail.fm**20140620003249 + Ignore-this: c28479b8a933cba263765bdddb112264 +] + +[define the domain of rational intervals +robdockins@fastmail.fm**20140619040809 + Ignore-this: 6cbe1a9cc690e5a9d77f37ee299154b + this domain is useful for describing the semantics of exact real arithmetic. +] + +[show that every effective CUSL is Plotkin +robdockins@fastmail.fm**20140619034433 + Ignore-this: d529a4b1d6d698f79572caa805072394 +] + +[fix notation for octothorpe +robdockins@fastmail.fm**20140614222130 + Ignore-this: 3dc815825f11ceaf4f4f53e4668e6382 +] + +[fix for coq 8.4pl4 +robdockins@fastmail.fm**20140614222049 + Ignore-this: 9745904845aaf54e5569df982fc93d65 +] + +[move swelling lemma into finsets +robdockins@fastmail.fm**20140504080535 + Ignore-this: ffa560e9aa4e4f8b15a55c1f9b1da72e +] + +[documentation improvements and code motion +robdockins@fastmail.fm**20140504070008 + Ignore-this: da7847f82403990342732a8ce226315c +] + +[replace the old finprod +robdockins@fastmail.fm**20140504005534 + Ignore-this: 606cf44422f68d66c8d2d90049e67b93 +] + +[remove the old finprod +robdockins@fastmail.fm**20140504005137 + Ignore-this: 38bd54e16c87d27bbede08496c37bfba +] + +[update st_lam_fix to use the new finprod +robdockins@fastmail.fm**20140504003627 + Ignore-this: 95d0a66e99ccead89bdfef09a1c8c109 +] + +[update st_lam to use the new termmodel +robdockins@fastmail.fm**20140503230854 + Ignore-this: c3d6b2155674b414c5c2e14b85b13760 +] + +[new version of finprod with a better term model +robdockins@fastmail.fm**20140503222035 + Ignore-this: db63e3a063bdb6f2f579644c7b63bd1b +] + +[a few more (hopefully final) lemmas about union +robdockins@fastmail.fm**20140422223924 + Ignore-this: 7b95c75abef9b0d45863b5e33d1c5a37 +] + +[finish proofs about union +robdockins@fastmail.fm**20140422065034 + Ignore-this: 2929c3cdb013c028a48022b0293b2f18 +] + +[powerdomain progress +robdockins@fastmail.fm**20140421064325 + Ignore-this: 592f9c6046f05a27897b460edb2efe10 + Show that powerdomains are endofunctors on PLT. Further, they are monads with + the 'singleton' and 'join' operations. Also make some progress on the additive + portion of the theory, dealing with emptyset and union. +] + +[tweak makefile +robdockins@fastmail.fm**20140420031337 + Ignore-this: d5954b26f731bfed3d79cefacab322fb +] + +[show that semvalue is the weakest condition allowing beta-reduction of strict functions +robdockins@fastmail.fm**20140420020447 + Ignore-this: 16a7ed23f04879f1fb324bdac8a2ffaf +] + +[some additional operations relating to the PLT adjunction +robdockins@fastmail.fm**20140420020351 + Ignore-this: db8eec6e3f74cce3acb67d2b660b104e +] + +[finish building power domain fmap +robdockins@fastmail.fm**20140420020217 + Ignore-this: 556e1cb87576de36cb26f8add3a1b163 +] + +[fix up st_lam.v +robdockins@fastmail.fm**20140329015058 + Ignore-this: 1c31d674b759fbd0cc74fb3125579f96 +] + +[push some proofs into finprod +robdockins@fastmail.fm**20140329000401 + Ignore-this: 49070fdd951e49473e60d3cd0ec431c6 +] + +[documentation and aesthetic changeds +robdockins@fastmail.fm**20140327043141 + Ignore-this: be27b24b78ea6af722a307117e59f5b3 +] + +[finish the st_lam_fix example +robdockins@fastmail.fm**20140322011153 + Ignore-this: e702f564b6eab2f8c11ab16bcb62504b +] + +[clarafications re: countable choice; remove unfinished example from build order +robdockins@fastmail.fm**20140321212852 + Ignore-this: 2a9d5c79c05ba088e1815feab99a5f6c +] + +[break the "fixes" operator into a separate file and prove some facts about it +robdockins@fastmail.fm**20140318013247 + Ignore-this: 80c506cef0719a974a049a1f5870f676 +] + +[minor fix to skiy.v +robdockins@fastmail.fm**20140317054057 + Ignore-this: ffef6fcaf5fa7f8cea80d2808caf4f4c +] + +[add the fixpoint operator; admit proofs +robdockins@fastmail.fm**20140317044648 + Ignore-this: 97ca18e980cdf46a9b40c8252badef14 +] + +[remove the evaluation case for variables +robdockins@fastmail.fm**20140317032932 + Ignore-this: e46d634e735e5b21a18518a48777168d +] + +[start on STLC with fixpoints -- but without fixpoints for now +robdockins@fastmail.fm**20140317031953 + Ignore-this: 3458bc18c73d967bef58418bc73e06cb +] + +[add the eliminator for booleans to st_lam; other additional utility lemmas +robdockins@fastmail.fm**20140317031753 + Ignore-this: 369dd375755cbd9ae5e3c969f3ef6ec +] + +[some minor code motion +robdockins@fastmail.fm**20140228064927 + Ignore-this: 804828472ddb0c5fafc72460fce8387b +] + +[plug final holes in st_lam and add to build order +robdockins@fastmail.fm**20140228044729 + Ignore-this: 3edc7f36bfa97775ba33ffa27c80df59 +] + +[reduce st_lam.v to facts I believe about fresh variables +robdockins@fastmail.fm**20140228010832 + Ignore-this: bde3e73291ddd32337d6fb999e4b1c02 +] + +[fix breakages +robdockins@fastmail.fm**20140226073930 + Ignore-this: 9be54f5255f8ed9d53a79260e9bdf565 +] + +[more work on lambdas +robdockins@fastmail.fm**20140226043753 + Ignore-this: 7f7452670221e2643067a3c7cc180998 +] + +[use new finprod implementation +robdockins@fastmail.fm**20140226043700 + Ignore-this: c9e05df5fcfd31254ed7318fe693490c +] + +[remove old finprod +robdockins@fastmail.fm**20140226043642 + Ignore-this: 2705703a2c782da21a152fbb27c8a972 +] + +[rearrange the interfact to finprod +robdockins@fastmail.fm**20140226043541 + Ignore-this: c44d7c478948f42b188eb8d06469abbf +] + +[fill remaining holes in finprod2 +robdockins@fastmail.fm**20140225205242 + Ignore-this: 1eeb9b8beef92790c28918292f2a9cf4 +] + +[rework some stuff dealing with semidecidable predicates +robdockins@fastmail.fm**20140225092149 + Ignore-this: 32b5ccb2927e08979ea92b9ef67c40f4 +] + +[lots of work on alpha-congrunce in lambdas +robdockins@fastmail.fm**20140225035601 + Ignore-this: fbbec9dac4cb328ff4e0b25df646e0c7 +] + +[terminate is universal in PLT +robdockins@fastmail.fm**20140225035538 + Ignore-this: abc6cd1a60578c435bf9ca596d8d0922 +] + +[new attack on nominal finite products +robdockins@fastmail.fm**20140225035516 + Ignore-this: 3875e713acc6aa5193696612f3ede76d +] + +[push forward a little on lambdas +robdockins@fastmail.fm**20140221095249 + Ignore-this: c690a1b03075702e3fd84aac7e268211 +] + +[update finprod for various changes +robdockins@fastmail.fm**20140221095230 + Ignore-this: a6d787930ed356ae2b0a003af1f4d44 +] + +[better discrete cases lemma +robdockins@fastmail.fm**20140219051301 + Ignore-this: f0ec88e8207257e7657ced933cf687e7 +] + +[start working on simply-typed lambdas +robdockins@fastmail.fm**20140219051238 + Ignore-this: 69bea345376ea39cd1addc0849a43077 +] + +[more messing about with advanced category theory stuff +robdockins@fastmail.fm**20140211095003 + Ignore-this: 9cd3c9d961349e8797f109f716c5f678 +] + +[minor rearrangements and code motion +robdockins@fastmail.fm**20140211041724 + Ignore-this: 642ad6f1395fde7ecd81e5a905fd5428 +] + +[some basic bicategory theory +robdockins@fastmail.fm**20140210083634 + Ignore-this: f47a898fa045a397d3ee70e1512b8baa +] + +[even more notation futzing +robdockins@fastmail.fm**20140209072416 + Ignore-this: d2061652cb3e80f6994f567a9e677b32 +] + +[additional notational futzing +robdockins@fastmail.fm**20140209043308 + Ignore-this: ac42cbbc94df227e6d5e70b96ae65fd3 +] + +[futz around with notations, various other cleanup activities +robdockins@fastmail.fm**20140209005551 + Ignore-this: 3f41a52650aadd956ac490b62e59c1c3 +] + +[complete adequacy for SKI+Y +robdockins@fastmail.fm**20140206050414 + Ignore-this: f730587ac7a42f3e35740976a1439f2e +] + +[minor changes in cpo +robdockins@fastmail.fm**20140206014745 + Ignore-this: 95244704faf1e6c336d62dc7912f9022 +] + +[push through most of SKI+Y adequacy +robdockins@fastmail.fm**20140205214805 + Ignore-this: dc998ef45f2e919e9373bfa21a5ef8c7 +] + +[major simplification of the adequacy proof for SKI +robdockins@fastmail.fm**20140205185605 + Ignore-this: f1f0dc46274db05f3393038dfe2775e2 +] + +[push forward on SKI+Y +robdockins@fastmail.fm**20140205044216 + Ignore-this: daf255aa940b42c1c68ba947a356370d +] + +[continue futzing with the LR statement +robdockins@fastmail.fm**20140203055601 + Ignore-this: f5ef9f06d3b1a11d76317b52cec691ab +] + +[start pushing on adequacy for SKI+Y +robdockins@fastmail.fm**20140202085948 + Ignore-this: 956844809340fad0c13c19e9fa729b5c +] + +[mostly finish soundness for SKI+Y +robdockins@fastmail.fm**20140202060633 + Ignore-this: 4c75fd9eeefa1d6dad6866662abea0fd +] + +[start working on a CCL example +robdockins@fastmail.fm**20140202020748 + Ignore-this: 44c5d7854cc19b0f90414c2be6b3df68 +] + +[make id(A) a parsing-only notation +robdockins@fastmail.fm**20140202020724 + Ignore-this: 68f51f754c0b89e2e815da47b901e4b1 +] + +[the PLT adjunction is strong monodial +robdockins@fastmail.fm**20140202020637 + Ignore-this: 7b29b9a6a5e8efa07440c528ec12d7bd +] + +[fix my broken version of lfp and fixup proofs +robdockins@fastmail.fm**20140202020615 + Ignore-this: 3ac283481318622cbf38378e815a4f09 +] + +[more work on SKI + Y +robdockins@fastmail.fm**20140202020516 + Ignore-this: d1f63e2ef610c6f93d03806c5426cfa5 +] + +[start work on SKI + Y +robdockins@fastmail.fm**20140201085039 + Ignore-this: fb7a405830cf90526cddd8ce37f4da40 +] + +[doc corrections +robdockins@fastmail.fm**20140130015908 + Ignore-this: bca4c04267bfdac8cb202651a0960d92 +] + +[lots of additional inline documentation +robdockins@fastmail.fm**20140129234834 + Ignore-this: ab2c59add5514f44a898de1f0eece98b +] + +[powerdomains form continuous functors in EMBED +robdockins@fastmail.fm**20140126234115 + Ignore-this: d2ee08902f0bdb52efd7f7ce2c594469 +] + +[complete the powerdomain constructions; build some operations +robdockins@fastmail.fm**20140125225202 + Ignore-this: 9c8f2632df05e84fc3794a338ff8720d +] + +[construct the basic powerdomains--still some holes left +robdockins@fastmail.fm**20140125064541 + Ignore-this: c3206d2e1e925096b3e9ff49afacef2f +] + +[generalize the lfp construction to a generic chain_sup operation +robdockins@fastmail.fm**20140124183103 + Ignore-this: 4cc2c1011b9f79365dcb7c76784fbfa6 +] + +[update makefile +robdockins@fastmail.fm**20140124073734 + Ignore-this: a0b7db8383262caa314c21b99e146222 +] + +[new file for recursive lambda domains +robdockins@fastmail.fm**20140124070023 + Ignore-this: 300c02b4da83b6ebd734aa2ccb21cd2d +] + +[more lemmas about antistrict homs +robdockins@fastmail.fm**20140124065953 + Ignore-this: 483c7b350dc3cab59c8ff50e1ac73b8c +] + +[fix breakage related to implicit arguments +robdockins@fastmail.fm**20140124065805 + Ignore-this: 561693d3280851299c6a49a2a34546b3 +] + +[notation tweaks in cpo.v +robdockins@fastmail.fm**20140124053800 + Ignore-this: 83e92d8c14568448074a940ceafbe2c9 +] + +[add if/then/else to the SKI system +robdockins@fastmail.fm**20140124023630 + Ignore-this: 37a9737932a05393a6338380226ca346 +] + +[case analysis for finite types +robdockins@fastmail.fm**20140124012505 + Ignore-this: 6ec1076b2a74f5832501a105a28a6dba +] + +[finish adequacy proof for SKI +robdockins@fastmail.fm**20140123211322 + Ignore-this: 1fe3e626e33431c27e2aa186b3bf91d2 +] + +[additional lemmas about domains +robdockins@fastmail.fm**20140123090037 + Ignore-this: fcad2dd816f805b8b5e7d1be3df60db8 +] + +[most of a proof of adequacy for SKI +robdockins@fastmail.fm**20140123085839 + Ignore-this: d1595c02a6387297018e7f316a3e751 +] + +[more work on finite products +robdockins@fastmail.fm**20140121061158 + Ignore-this: c2f8212e041478104dd4c81c225b42d5 +] + +[begin work on a more flexible "finprod" domain +robdockins@fastmail.fm**20140119021653 + Ignore-this: 249718a2c31964733171b21c84d2effb +] + +[mess with implicit arguments in categories.v +robdockins@fastmail.fm**20140113041450 + Ignore-this: 314cad9207f706e949bd686aaa5c5e1b +] + +[products for CPO, uniformity of lfp +robdockins@fastmail.fm**20140113041421 + Ignore-this: e533abe995e634c732a35e71d66ddb6a +] + +[define the LFP in pointed CPOs, prove the Scott induction principle +robdockins@fastmail.fm**20140112231843 + Ignore-this: 2014174b1c6914bef376d614f34d073f +] + +[build the forgetful functor from EMBED to PLT +robdockins@fastmail.fm**20140110014909 + Ignore-this: 1dacbfc0383e48f4ab35fe0a5fd11cec +] + +[notation changes, prove sum_cases and curry preserve order and equality +robdockins@fastmail.fm**20140110014820 + Ignore-this: d1c6a1d0346a9eba14f3529ac30b5e2f +] + +[prove addl facts about pairs, tweak implicit arguments +robdockins@fastmail.fm**20140110010319 + Ignore-this: 9f0af8abc268b2b22d8b5450d6a4136 +] + +[make 'ob' a coercion +robdockins@fastmail.fm**20140110010204 + Ignore-this: 467c0b0a8b086a7f44bf98875a4380d6 +] + +[copyright notices +robdockins@fastmail.fm**20140106232333 + Ignore-this: f59bafa0ec99e259bd9b4319f2cdbc67 +] + +[add ord_dec coercion +robdockins@fastmail.fm**20140104052750 + Ignore-this: 4ed1cacfd27979f0fe518862be5ac27c +] + +[define the model for CBV lambda calculus +robdockins@fastmail.fm**20140104050626 + Ignore-this: 88ca796d4697bfebb044d3fae27d6129 +] + +[proof a fixpoint lemma for unpointed domains +robdockins@fastmail.fm**20140103231818 + Ignore-this: 4939eb02d09b6a4eecf145c887c64393 +] + +[prove that the adjoint functors between PLT and PPLT extend to continuous functors in EMBED +robdockins@fastmail.fm**20140103000915 + Ignore-this: 54da0101f581731ebe512ed514e0603e +] + +[notation changes for PLT +robdockins@fastmail.fm**20140102234446 + Ignore-this: ad1f82f22d1bf0e057f11c3508a81716 +] + +[move embeddings into their own file; pull TPLT and PPLT into profinite.v +robdockins@fastmail.fm**20140102234424 + Ignore-this: 3704996af47ae32415ba3e539d67cf5c +] + +[Show that PLT is cocartesian; rearrange proof that EMBED(true) is terminated +robdockins@fastmail.fm**20140102213805 + Ignore-this: 3470df6910e7a3e4bda478c0c6ecea62 +] + +[remove unnecessary "inh" hypothesis in the definition of Plotkin order; fixup the fallout +robdockins@fastmail.fm**20140102213646 + Ignore-this: b6a5ad59296f938b377d71852120d48b +] + +[move proofs that empty and unit preorders are effective plotkin +robdockins@fastmail.fm**20140102205530 + Ignore-this: 7324843510fd938d356aa82003c9ec68 +] + +[make epi/mono/iso morphisms into categories +robdockins@fastmail.fm**20131228082442 + Ignore-this: ee75a2b6eb1f3d6fa47f17d6734e5015 +] + +[define the cocartesian and distributive categories +robdockins@fastmail.fm**20131226001612 + Ignore-this: 11e9d8a88bef42bcb800b31d85d28d16 +] + +[remove uses of maximally implict arguments +robdockins@fastmail.fm**20131226001536 + Ignore-this: c0d93a5398aea58cbcc4fbbca3b59b17 +] + +[fixpoints and binary sums for NOMINAL +robdockins@fastmail.fm**20131121092931 + Ignore-this: 8a660dfe2ab16a8208ae559dcf2b7ed0 +] + +[modify bilimit.v to use the general construction from cont_functors.v +robdockins@fastmail.fm**20131120075848 + Ignore-this: 17ea36107ade1646eab5c99aec3561a9 +] + +[generic fixpoint construction for categories with initial objects and directed colimits +robdockins@fastmail.fm**20131119092522 + Ignore-this: 25674dff855a1cecdb4ee919f8bf3a5d +] + +[remove some irritating unit parameters, fix doc typos +robdockins@fastmail.fm**20131118093204 + Ignore-this: 38342d58567d8a13471620d5b7c2b7d4 +] + +[improvements to categories; complete some constructions in nominal +robdockins@fastmail.fm**20131118085737 + Ignore-this: e58cb49a01d0210dabdb021250910adb +] + +[build fixes +robdockins@fastmail.fm**20131113004305 + Ignore-this: 5abffcd1d6b44f816749c5e0cfd5b6e9 +] + +[Documentation additions +robdockins@fastmail.fm**20131113004254 + Ignore-this: 79a913d3a8652866f3fdc64891f6304d +] + +[lots of inline documentation additions +robdockins@fastmail.fm**20131112192736 + Ignore-this: 6aa38112c10ceed3bf43e35dbda98312 +] + +[update makefiles +robdockins@fastmail.fm**20131112192706 + Ignore-this: d834beaa532cdf994cfa0a0b5a562e4f +] + +[continuous functors for binary sum and products +robdockins@fastmail.fm**20131112192605 + Ignore-this: 61520e6e315df909465a02f854816366 +] + +[add the category of nominal types +robdockins@fastmail.fm**20131112192520 + Ignore-this: f0351c5eb0bdacdfe192a6863d9c0bc6 +] + +[split the proof that expF is a continuous functor into a separate file; rearrange some defintions +robdockins@fastmail.fm**20130924013328 + Ignore-this: 4eacee37bb6474d1bdfffe416b98b4c1 +] + +[rearrange definitions of continuous functors. Prove enough plumbing to build the model: D = D->D +robdockins@fastmail.fm**20130924002837 + Ignore-this: a66f9e8833601e244048b70e8bfaab96 +] + +[show that the function space is a continuous functor; other junk +robdockins@fastmail.fm**20130923060521 + Ignore-this: d8f406450688c633ebc1fe1eb0343c91 +] + +[some name changes, other cosmetic fixes +robdockins@fastmail.fm**20130909043234 + Ignore-this: cdd24d1c96a34fb3573c1806153df9fb +] + +[additional cosmetic changes and rearrangements +robdockins@fastmail.fm**20130909020137 + Ignore-this: 77d28bc9452f6c93915194033118dab7 +] + +[reorganize profinite code +robdockins@fastmail.fm**20130909011437 + Ignore-this: 8511bf92ca6998ff8c69d5537624bdb8 +] + +[cosmetic changes +robdockins@fastmail.fm**20130908183909 + Ignore-this: e19039701e58fd26ca4eab79d7b49d14 +] + +[complete the bilimit construction, show how to take fixpoints of continuous functors +robdockins@fastmail.fm**20130908175228 + Ignore-this: 82feab8fdc0c944f13d91605c6a8e571 +] + +[find a MUCH easier path to a bilimit construction +robdockins@fastmail.fm**20130907012151 + Ignore-this: fcc72ad140b045ef37e4b03ad38a8fb0 +] + +[lots of progress, mostly on defining bilimits +robdockins@fastmail.fm**20130905204959 + Ignore-this: abf4bcf03a49fa009f9fb2200ee3abf2 +] + +[start working on the theory of finite preorders, which form a basis for plokin orders +robdockins@fastmail.fm**20130812054451 + Ignore-this: 5be36257a8fdf486bcc31f587d93c457 +] + +[parameterize plotkin orders, build category PPLT +robdockins@fastmail.fm**20130811063623 + Ignore-this: 3f273841bc72098acee0fd618627dbd5 +] + +[complete the details showing PLT is cartesian closed +robdockins@fastmail.fm**20130809230336 + Ignore-this: 13fd1b5a8172dd263cf655421f7584f7 +] + +[add files missed in the first import +robdockins@fastmail.fm**20130809080742 + Ignore-this: 6b59cce866a486d70559f7c80fe99053 +] + +[initial import of development +robdockins@fastmail.fm**20130809080409 + Ignore-this: 44cb5a0df2f1643d289f07dcd4227cbf + First major steps toward a fully effective and usable formalized + domain theory. We formalize the plotkin preorders and show that + they form a cartesian closed category. +] diff --git a/pkgs/development/coq-modules/domains/default.nix b/pkgs/development/coq-modules/domains/default.nix new file mode 100644 index 000000000000..975260c839bd --- /dev/null +++ b/pkgs/development/coq-modules/domains/default.nix @@ -0,0 +1,26 @@ +{stdenv, fetchdarcs, coq}: + +stdenv.mkDerivation rec { + + name = "coq-domains-${coq.coq-version}-${version}"; + version = "ce1a9806"; + + src = fetchdarcs { + url = http://hub.darcs.net/rdockins/domains; + context = ./darcs_context; + sha256 = "0zdqiw08b453i8gdxwbk7nia2dv2r3pncmxsvgr0kva7f3dn1rnc"; + }; + + buildInputs = [ coq.ocaml coq.camlp5 ]; + propagatedBuildInputs = [ coq ]; + + installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}/"; + + meta = with stdenv.lib; { + homepage = http://rwd.rdockins.name/domains/; + description = "A Coq library for domain theory"; + maintainers = with maintainers; [ jwiegley ]; + platforms = coq.meta.platforms; + }; + +} diff --git a/pkgs/development/coq-modules/heq/default.nix b/pkgs/development/coq-modules/heq/default.nix index 581941b2249d..5f31fe6dc341 100644 --- a/pkgs/development/coq-modules/heq/default.nix +++ b/pkgs/development/coq-modules/heq/default.nix @@ -15,7 +15,7 @@ stdenv.mkDerivation rec { preBuild = "cd src"; - installFlags = "COQLIB=$out/lib/coq/${coq.coq-version}"; + installFlags = "COQLIB=$(out)/lib/coq/${coq.coq-version}"; meta = with stdenv.lib; { homepage = https://www.mpi-sws.org/~gil/Heq/; diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix index d9dafc964e35..389bcce9b02d 100644 --- a/pkgs/top-level/all-packages.nix +++ b/pkgs/top-level/all-packages.nix @@ -11600,6 +11600,8 @@ let coqExtLib = callPackage ../development/coq-modules/coq-ext-lib {}; + domains = callPackage ../development/coq-modules/domains {}; + heq = callPackage ../development/coq-modules/heq {}; mathcomp = callPackage ../development/coq-modules/mathcomp {};