diff options
| -rw-r--r-- | pkgs/build-support/fetchdarcs/builder.sh | 5 | ||||
| -rw-r--r-- | pkgs/build-support/fetchdarcs/default.nix | 14 | ||||
| -rw-r--r-- | pkgs/development/compilers/idris/default.nix | 24 | ||||
| -rw-r--r-- | pkgs/development/compilers/idris/idris.context | 586 | ||||
| -rw-r--r-- | pkgs/development/libraries/haskell/ivor/default.nix | 12 | ||||
| -rw-r--r-- | pkgs/top-level/haskell-packages.nix | 9 |
6 files changed, 640 insertions, 10 deletions
diff --git a/pkgs/build-support/fetchdarcs/builder.sh b/pkgs/build-support/fetchdarcs/builder.sh index 7214eda4266..a211de42da4 100644 --- a/pkgs/build-support/fetchdarcs/builder.sh +++ b/pkgs/build-support/fetchdarcs/builder.sh @@ -5,11 +5,14 @@ tagflags="" if test -n "$tag"; then tagtext="(tag $tag) " tagflags="--tag=$tag" +elif test -n "$context"; then + tagtext="(context) " + tagflags="--context=$context" fi header "getting $url $partial ${tagtext} into $out" -darcs get --no-pristine-tree $partial $tagflags "$url" "$out" +darcs get --lazy --ephemeral $tagflags "$url" "$out" # remove metadata, because it can change rm -rf "$out/_darcs" diff --git a/pkgs/build-support/fetchdarcs/default.nix b/pkgs/build-support/fetchdarcs/default.nix index b8dde18aa3e..63e4ecde88a 100644 --- a/pkgs/build-support/fetchdarcs/default.nix +++ b/pkgs/build-support/fetchdarcs/default.nix @@ -1,17 +1,13 @@ -{stdenv, darcs, nix}: {url, tag ? null, md5, partial ? true}: +{stdenv, darcs, nix}: {url, tag ? null, context ? null, md5 ? "", sha256 ? ""}: stdenv.mkDerivation { name = "fetchdarcs"; builder = ./builder.sh; - buildInputs = [darcs nix]; - partial = if partial then "--partial" else ""; + buildInputs = [darcs]; - # Nix <= 0.7 compatibility. - id = md5; - - outputHashAlgo = "md5"; + outputHashAlgo = if sha256 == "" then "md5" else "sha256"; outputHashMode = "recursive"; - outputHash = md5; + outputHash = if sha256 == "" then md5 else sha256; - inherit url tag; + inherit url tag context; } diff --git a/pkgs/development/compilers/idris/default.nix b/pkgs/development/compilers/idris/default.nix new file mode 100644 index 00000000000..e8afd86463d --- /dev/null +++ b/pkgs/development/compilers/idris/default.nix @@ -0,0 +1,24 @@ +{fetchdarcs, cabal, mtl, parsec, readline, ivor, happy}: + +cabal.mkDerivation (self : { + pname = "idris"; + name = self.fname; + version = "0.1.2"; + src = fetchdarcs { + url = http://www-fp.dcs.st-and.ac.uk/~eb/darcs/Idris; + sha256 = "de50ed4bedacee36d9942bf4db90deca3915cf6c106aa834d11e83972b2b639a"; + context = ./idris.context; + }; + propagatedBuildInputs = [mtl parsec readline ivor]; + extraBuildInputs = [happy]; + preConfigure = '' + echo "module Idris.Prefix where prefix = \"$out\"" > Idris/Prefix.hs + ''; + postInstall = '' + ensureDir $out/lib/idris + install lib/*.idr lib/*.e $out/lib/idris + ''; + meta = { + description = "An experimental language with full dependent types"; + }; +}) diff --git a/pkgs/development/compilers/idris/idris.context b/pkgs/development/compilers/idris/idris.context new file mode 100644 index 00000000000..fad67499883 --- /dev/null +++ b/pkgs/development/compilers/idris/idris.context @@ -0,0 +1,586 @@ + +Context: + +[Missed SCTrans source! +eb@cs.st-andrews.ac.uk**20090511120315] + +[Put RunIO in a more sensible place +eb@cs.st-andrews.ac.uk**20090426144418] + +[Update cabal details +eb@cs.st-andrews.ac.uk**20090426144101] + +[Convert things which look like Nats to Nats for optimisation +eb@cs.st-andrews.ac.uk**20090423220551] + +[Basic Nat optimisation +eb@cs.st-andrews.ac.uk**20090423185609] + +[need to check if arguments are still needed to discriminate on collapsing +eb@cs.st-andrews.ac.uk**20090309174234] + +[Using knowledge of collapsing to help forcing +eb@cs.st-andrews.ac.uk**20090309153744] + +[Make transforms part of state, and display of optimised terms +eb@cs.st-andrews.ac.uk**20090309145419] + +[Prettier time formatting +eb@cs.st-andrews.ac.uk**20090309131334] + +[Don't just crash if the command is invalid... +eb@cs.st-andrews.ac.uk**20090309125424] + +[Added global options +eb@cs.st-andrews.ac.uk**20090309124541 + :o sets, :o f- or :o f+ to turn forcing/collapsing off/on + :o r- or :o r+ to turn display of compile/run times off/on +] + +[Added collapsing optimisation +eb@cs.st-andrews.ac.uk**20090309112238] + +[Added unused argument elimination +eb@cs.st-andrews.ac.uk**20090309004741 + Can fit within the optimisation framework, but you need to remember + the transforms so far at each definition for maximum effect. +] + +[(Failed) effort at argument erasure +eb@cs.st-andrews.ac.uk**20090308222948 + Trying to get it into the same framework as constructor transformations, + but it isn't going to happen that easily. +] + +[Added forcing optimisation +eb@cs.st-andrews.ac.uk**20090308164110] + +[Decide tactic works out its arguments +eb@cs.st-andrews.ac.uk**20090305165743] + +[Allow redefining of do notation +eb@cs.st-andrews.ac.uk**20090228164646] + +[lookupIdx fix +eb@cs.st-andrews.ac.uk**20090227231257] + +[Added 'using' syntax +eb@cs.st-andrews.ac.uk**20090226003439 + For blocks where lots of things use the same implicit arguments, saving + lots of typing and clutter. + (also allowed forward declaration of datatypes) +] + +[Fix conflict +eb@cs.st-andrews.ac.uk**20090107121727] + +[Laziness annotations +eb@cs.st-andrews.ac.uk**20090107121328] + +[Added decide tactic +eb@cs.st-andrews.ac.uk**20081220221809] + +[Add 'collapsible' flag +eb@cs.st-andrews.ac.uk**20081219180742] + +[Add TODO +eb@cs.st-andrews.ac.uk**20081219180726] + +[Some compiler fiddling +eb@cs.st-andrews.ac.uk**20081219155920] + +[Keep track of names which are still to be proved +eb@cs.st-andrews.ac.uk**20081219143302] + +[File operations +eb@cs.st-andrews.ac.uk**20081218233527] + +[Can allow the system to make up names for metavariables +eb@cs.st-andrews.ac.uk**20081218233428] + +[Deal with c includes and external libraries +eb@cs.st-andrews.ac.uk**20081126150921] + +[Fix foreign functions for IO +eb@cs.st-andrews.ac.uk**20081102153832] + +[Added Ptr primitive +eb@cs.st-andrews.ac.uk**20081102134232] + +[Add unsafePerformIO +eb@cs.st-andrews.ac.uk**20081019171546 + Mostly meant for pure foreign functions, but of course you're free to abuse + it as you like... +] + +[Add flags on functions to denote special behaviour +eb@cs.st-andrews.ac.uk**20081019160020 + Specifically, so far: + * %nocg Never generate code when compling + * %eval Evaluate completely before compiling + + This allows some 'meta-programs' to be written, which are fully evaluated + before compiling. We use this for defining foreign functions easily. +] + +[Record paper changes! +eb@cs.st-andrews.ac.uk**20080916170851] + +[Added 'use' tactic +eb@cs.st-andrews.ac.uk**20080916170742 + Like 'believe' but instead of just believing the value, adds subgoals for + each required equality proof. +] + +[More of paper +eb@cs.st-andrews.ac.uk**20080901161738] + +[Added paper macros +eb@cs.st-andrews.ac.uk**20080901094433] + +[Starting on paper +eb@cs.st-andrews.ac.uk**20080829091345] + +[Compiling 'Foreign' constructor (but only when inline) +eb@cs.st-andrews.ac.uk**20080826123458] + +[Generate Idris functions from foreign function descriptions +eb@cs.st-andrews.ac.uk**20080825164523] + +[Some work towards constructor optimisations +eb@cs.st-andrews.ac.uk**20080825094709] + +[Basic foreign function framework +eb@cs.st-andrews.ac.uk**20080825094631] + +[Added test transformation on Vects +eb@cs.st-andrews.ac.uk**20080731155217] + +[Transformation application +eb@cs.st-andrews.ac.uk**20080730125618] + +['noElim' flag to allow big data types not to need elimination rules +eb@cs.st-andrews.ac.uk**20080729125140] + +[Added __toInt and __toString +eb@cs.st-andrews.ac.uk**20080710151313 + Hacky for now, until we work out a nice way of doing coercions between + primitives. But it makes some programs, like those which ask for an int + as input, possible. +] + +[If an operator returns a boolean, the compiler had better make code to build a boolean! +eb@cs.st-andrews.ac.uk**20080710145313] + +[Deal with weird names that Ivor generates in the compiler +eb@cs.st-andrews.ac.uk**20080709112032] + +[Some Nat theorems +eb@cs.st-andrews.ac.uk**20080709014158] + +[Generalise tactic +eb@cs.st-andrews.ac.uk**20080709014121] + +[Need to give all the definitions to addIvor +eb@cs.st-andrews.ac.uk**20080708203624] + +[Don't crash when there's an error in input! +eb@cs.st-andrews.ac.uk**20080708182610] + +[Only allow 'believe' to rewrite values +eb@cs.st-andrews.ac.uk**20080708165140 + This way at least the types have to be right before '?=' defined + programs will run. +] + +[Added 'believe' tactic +eb@cs.st-andrews.ac.uk**20080708160736 + For allowing the testing of programs before a complete proof term + exists. Obviously programs built this way are not trustworthy! They make + use of a "Suspend_Disbelief" function which just invents a rewrite rule + that works, but which doesn't have a proof. +] + +[Added '?=' syntax +eb@cs.st-andrews.ac.uk**20080708140505 + If you have a pattern clause, and don't know the definite type of the + right hand side, use; + foo patterns ?= def; [theoremName] + + This will add a theorem called theoremName which fixes up the type, + and you can prove it later, via :p or with the 'proof' syntax. Useful + if you want to hide details of the proof of a necessary rewriting. +] + +[Catch errors in proofs, and allow abandoning +eb@cs.st-andrews.ac.uk**20080708123202] + +[Identify parameters of data types to make elimination rule properly +eb@cs.st-andrews.ac.uk**20080708105930] + +[Reading of proof scripts +eb@cs.st-andrews.ac.uk**20080707010718] + +[Add Undo, require % before tactics, and output script when done +eb@cs.st-andrews.ac.uk**20080707004642] + +[Rudimentary theorem prover now working +eb@cs.st-andrews.ac.uk**20080706235523] + +[Parsing tactics and proofs +eb@cs.st-andrews.ac.uk**20080706222536] + +[Adding some tactics +eb@cs.st-andrews.ac.uk**20080706211202] + +[Added :e command and call to epic +eb@cs.st-andrews.ac.uk**20080702115125] + +[forking needs the argument to be lazily evaluated +eb@cs.st-andrews.ac.uk**20080630141845] + +[Added threading to compiler +eb@cs.st-andrews.ac.uk**20080630130045] + +[Compiling IORefs +eb@cs.st-andrews.ac.uk**20080630123521] + +[Add Prelude.e, and prepend it to epic output +eb@cs.st-andrews.ac.uk**20080630113450] + +[Added Prover.lhs (not that it does much yet) +eb@cs.st-andrews.ac.uk**20080623231341] + +[Fix constructor expansion +eb@cs.st-andrews.ac.uk**20080623111226] + +[Got the basic compilation working +eb@cs.st-andrews.ac.uk**20080622233141] + +[Added proof token to Lexer +eb@cs.st-andrews.ac.uk**20080516140747 + (not doing anything yet, it needs a separate parser) + Also fix minor lexing error, and added ':i' command to drop into Ivor + for debugging purposes. +] + +[Added 'normalise' command +eb@cs.st-andrews.ac.uk**20080523140332 + Useful if you want to normalise an IO computation without running it. +] + +[Small implicit argument change +eb@cs.st-andrews.ac.uk**20080513231721 + {a,b,c} now allowed (i.e no need for type label as in {a,b,c:_} + Also, implicit arguments can now, syntactically, only appear at the + left of types of top level declarations (since that is the only place they + make sense with our simple way of handling such arguments). +] + +['!' to stop implicit arguments being added to a name +eb@cs.st-andrews.ac.uk**20080513215523] + +[Outputting Epic code +eb@cs.st-andrews.ac.uk**20080511173955 + Still some things to sort out before this runs though +] + +[Removing IO boiler plate for compilation +eb@cs.st-andrews.ac.uk**20080510170038] + +[Lambda lifter +eb@cs.st-andrews.ac.uk**20080509161049] + +[Oops, broke the build *again* +eb@cs.st-andrews.ac.uk**20080508220834] + +[Data type for result of lambda lifting +eb@cs.st-andrews.ac.uk**20080508214635] + +[Compiler part 1 (pattern matching) +eb@cs.st-andrews.ac.uk**20080508200113] + +[partition +eb@cs.st-andrews.ac.uk**20080508132348] + +[Let's try not to apply patches which break the build... +eb@cs.st-andrews.ac.uk**20080508111341] + +[Patterns representation +eb@cs.st-andrews.ac.uk**20080508110025] + +[Added append to library +eb@cs.st-andrews.ac.uk**20080429111614] + +[Begin planning compiler +eb@cs.st-andrews.ac.uk**20080414123534] + +[brief note +eb@cs.st-andrews.ac.uk**20080414103207] + +[Minor LaTeX improvement +eb@cs.st-andrews.ac.uk**20080330151806 + Output placeholders correctly. Can you tell I'm writing a paper ;). +] + +[Even more LaTeX fixes +eb@cs.st-andrews.ac.uk**20080327115445] + +[Fix some LaTeXing +eb@cs.st-andrews.ac.uk**20080327113804] + +[Some latex tidying +eb@cs.st-andrews.ac.uk**20080325114709] + +[Latex of do notating +eb@cs.st-andrews.ac.uk**20080325110051] + +[Add %latex directive to parser +eb@cs.st-andrews.ac.uk**20080325105552] + +[Allow giving latex commands for particular names in :l +eb@cs.st-andrews.ac.uk**20080325103351] + +[Basic LaTeX generation working +eb@cs.st-andrews.ac.uk**20080324185632] + +[Started LaTeX generation +eb@cs.st-andrews.ac.uk**20080324170817] + +[Implement :t in REPL +eb@cs.st-andrews.ac.uk**20080324143135] + +[Use readline for REPL, add :commands +eb@cs.st-andrews.ac.uk**20080324141759] + +[Oops, didn't mean to record the trace +eb@cs.st-andrews.ac.uk**20080322115632] + +[Allow types on bindings in do notation +eb@cs.st-andrews.ac.uk**20080322114909] + +[Fix bug: add placeholders inside infix ops +eb@cs.st-andrews.ac.uk**20080320150127] + +[Pretty print refl +eb@cs.st-andrews.ac.uk**20080320134148] + +[Bind multiple names in one go in type declarations +eb@cs.st-andrews.ac.uk**20080320132941] + +[Locks are semaphores +eb@cs.st-andrews.ac.uk**20080319161532 + So allow them to be initialised with the number of processes allowed to + hold onto then, +] + +[Missed a case in constant show +eb@cs.st-andrews.ac.uk**20080318175442] + +[Add Maybe and Either to prelude +eb@cs.st-andrews.ac.uk**20080318224740] + +[Use 'fastCheck' since we already know our IO programs work +eb@cs.st-andrews.ac.uk**20080318161100] + +[Pretty printing and parsing tweaks +eb@cs.st-andrews.ac.uk**20080318161027] + +[No point in generating elimination rules since we don't use them +eb@cs.st-andrews.ac.uk**20080317162738 + Perhaps later, if linking to a theorem prover, it will be useful, but + it can be done on demand. +] + +[Dump environment for metavars in the right order +eb@cs.st-andrews.ac.uk**20080315230225] + +[Nicer display of metavariables +eb@cs.st-andrews.ac.uk**20080314174637] + +[Added a pretty ugly pretty-printer for terms +eb@cs.st-andrews.ac.uk**20080314154034] + +[Added metavariable syntax +eb@cs.st-andrews.ac.uk**20080314132802] + +[Back in sync with Ivor (addPatternDef type changed) +eb@cs.st-andrews.ac.uk**20080314011920] + +[Add modules to .cabal for executable +eb@cs.st-andrews.ac.uk**20080313134204] + +[imports in RunIO +eb@cs.st-andrews.ac.uk**20080312174755] + +[minor cabal format +gwern0@gmail.com**20080312041116] + +[improve cabal metadata for hackage, split into lib/main +gwern0@gmail.com**20080312041034] + +[fix sdist +gwern0@gmail.com**20080312040218] + +[+Extensions +gwern0@gmail.com**20080312035953] + +[Context.lhs -> Context.hs +gwern0@gmail.com**20080312035926 + Literate files are just wasteful if they aren't literate +] + +[dehaskell98 +gwern0@gmail.com**20080312035905] + +[Update ioref example +eb@cs.st-andrews.ac.uk**20080312125024] + +[Added IORefs +eb@cs.st-andrews.ac.uk**20080312123834] + +[Added some concurrency primitives +eb@cs.st-andrews.ac.uk**20080311205546 + fork, newLock, lock, unlock +] + +[Add simple stateful DSL +eb@cs.st-andrews.ac.uk**20080311151020] + +[Add placeholders in do expressions too! +eb@cs.st-andrews.ac.uk**20080311150824] + +[Be more implicit! +eb@cs.st-andrews.ac.uk**20080310135937] + +[Better if testVect has ints +eb@cs.st-andrews.ac.uk**20080310133325] + +[syntax tinker in partition.idr +eb@cs.st-andrews.ac.uk**20080310132921] + +[Syntax for let bindings +eb@cs.st-andrews.ac.uk**20080310025357] + +[if...then...else syntax +eb@cs.st-andrews.ac.uk**20080310024516] + +[Member predicate +eb@cs.st-andrews.ac.uk**20080310013200] + +[Syntax for _ patterns +eb@cs.st-andrews.ac.uk**20080310012608] + +[Rename List +eb@cs.st-andrews.ac.uk**20080310002023] + +[builtins needs bool +eb@cs.st-andrews.ac.uk**20080310001809] + +[Removed samples which should be in lib +eb@cs.st-andrews.ac.uk**20080309224149] + +[Added io example +eb@cs.st-andrews.ac.uk**20080309223957] + +[More keeping in sync with Ivor +eb@cs.st-andrews.ac.uk**20080309222931] + +[Take advantage of better ivor inference +eb@cs.st-andrews.ac.uk**20080309213603] + +[Added vect lib +eb@cs.st-andrews.ac.uk**20080308185405] + +[Added List to library +eb@cs.st-andrews.ac.uk**20080308185119] + +[Lambdas can take multiple arguments +eb@cs.st-andrews.ac.uk**20080308185050] + +[Added integer comparison operators +eb@cs.st-andrews.ac.uk**20080308134245] + +[Add polymorphic boolean equality +eb@cs.st-andrews.ac.uk**20080308133304] + +[Added library paths and a simple prelude +eb@cs.st-andrews.ac.uk**20080308132011] + +[Some primitive operators, and '=' for JM equality +eb@cs.st-andrews.ac.uk**20080307234257] + +[Use WHNF for evaluation now Ivor has it +eb@cs.st-andrews.ac.uk**20080307195902] + +[Added builtins +eb@cs.st-andrews.ac.uk**20080307173517] + +[add RunIO.hs +eb@cs.st-andrews.ac.uk**20080306114827] + +[Added more samples (IO not quite working yet due to Ivor bug though) +eb@cs.st-andrews.ac.uk**20080305170333] + +[Add do notation +eb@cs.st-andrews.ac.uk**20080305170312] + +['include' files +eb@cs.st-andrews.ac.uk**20080305112534] + +[Latest Ivor allows more implicitness +eb@cs.st-andrews.ac.uk**20080305104707] + +[Enough annotations to make interp work +eb@cs.st-andrews.ac.uk**20080305001951] + +[Allow forward declarations for functions, add quicksort example +eb@cs.st-andrews.ac.uk**20080305000656] + +[Added 'partition' example +eb@cs.st-andrews.ac.uk**20080304224512] + +[Easier to put implicit arguments in pattern clauses +eb@cs.st-andrews.ac.uk**20080304224425] + +[John Major equality syntax +eb@cs.st-andrews.ac.uk**20080304215146] + +[Added interpreter example, fixed simple sample +eb@cs.st-andrews.ac.uk**20080303164114] + +[Changed some syntax +eb@cs.st-andrews.ac.uk**20080303163946 + - Implicit arguments can now be named when applied, so that the parser + knows which argument you mean + - No need for {} around definitions + - Type of types is # + +] + +[make sure constructur arguments get new names generated +eb@cs.st-andrews.ac.uk**20080229003215] + +[Added samples directory +eb@cs.st-andrews.ac.uk**20080228232920] + +[First version which runs code! +eb@cs.st-andrews.ac.uk**20080228232820] + +[Some simple examples +eb@cs.st-andrews.ac.uk**20080228175453] + +[Now building terms and datatypes for Ivor with implicit args added +eb@cs.st-andrews.ac.uk**20080228161136] + +[More work on parser; constants, lambdas, new syntax tree +eb@cs.st-andrews.ac.uk**20080226111951] + +[Parser for datatypes and basic function definitions +eb@cs.st-andrews.ac.uk**20080108171829] + +[Started parser +eb@cs.st-andrews.ac.uk**20071214181416] + +[First chunk of code +eb@cs.st-andrews.ac.uk**20071212114523] diff --git a/pkgs/development/libraries/haskell/ivor/default.nix b/pkgs/development/libraries/haskell/ivor/default.nix new file mode 100644 index 00000000000..d010707ac00 --- /dev/null +++ b/pkgs/development/libraries/haskell/ivor/default.nix @@ -0,0 +1,12 @@ +{cabal, mtl, parsec}: + +cabal.mkDerivation (self : { + pname = "ivor"; + version = "0.1.8"; + sha256 = "e51ad07c78ea0cad6fce9253012258dbf7c740198792aa4a446e1f0269a9186d"; + propagatedBuildInputs = [mtl parsec]; + meta = { + description = "Theorem proving library based on dependent type theory"; + }; +}) + diff --git a/pkgs/top-level/haskell-packages.nix b/pkgs/top-level/haskell-packages.nix index cef0f36978d..3b635455d64 100644 --- a/pkgs/top-level/haskell-packages.nix +++ b/pkgs/top-level/haskell-packages.nix @@ -153,6 +153,15 @@ rec { inherit cabal; }; + idris = import ../development/compilers/idris { + inherit cabal mtl parsec readline ivor happy; + inherit (pkgs) fetchdarcs; + }; + + ivor = import ../development/libraries/haskell/ivor { + inherit cabal mtl parsec; + }; + json = import ../development/libraries/haskell/json { inherit cabal mtl; }; |