Updating from trunk
svn path=/nixpkgs/branches/stdenv-updates/; revision=24038
This commit is contained in:
Lluís Batlle i Rossell
@@ -11,4 +11,9 @@ stdenv.mkDerivation {
|
||||
|
||||
inherit jre;
|
||||
buildInputs = [jre];
|
||||
|
||||
meta = {
|
||||
homepage = http://www.eclipse.org/aspectj/;
|
||||
description = "A seamless aspect-oriented extension to the Java programming language";
|
||||
};
|
||||
}
|
||||
|
||||
14
pkgs/development/compilers/epic/default.nix
Normal file
14
pkgs/development/compilers/epic/default.nix
Normal file
@@ -0,0 +1,14 @@
|
||||
{cabal, mtl, happy, gmp, boehmgc}:
|
||||
|
||||
cabal.mkDerivation (self : {
|
||||
pname = "epic";
|
||||
version = "0.1.5";
|
||||
sha256 = "5a3d94e88cb85beb3c13f3b9f3c00c6768e1b067ff88d40ea63d9961a92347ff";
|
||||
propagatedBuildInputs = [mtl];
|
||||
extraBuildInputs = [happy gmp boehmgc];
|
||||
meta = {
|
||||
description = "An experimental language with full dependent types";
|
||||
license = "BSD";
|
||||
maintainers = [self.stdenv.lib.maintainers.andres];
|
||||
};
|
||||
})
|
||||
87
pkgs/development/compilers/eql/default.nix
Normal file
87
pkgs/development/compilers/eql/default.nix
Normal file
@@ -0,0 +1,87 @@
|
||||
x@{builderDefsPackage
|
||||
, fetchgit, qt4, ecl
|
||||
, ...}:
|
||||
builderDefsPackage
|
||||
(a :
|
||||
let
|
||||
helperArgNames = ["stdenv" "fetchurl" "builderDefsPackage"] ++
|
||||
["fetchgit"];
|
||||
|
||||
buildInputs = map (n: builtins.getAttr n x)
|
||||
(builtins.attrNames (builtins.removeAttrs x helperArgNames));
|
||||
sourceInfo = rec {
|
||||
method = "fetchgit";
|
||||
rev = "7bd32f49c9965d8f7dc262a0f265b153b0a81ced";
|
||||
url = "git://gitorious.org/eql/eql";
|
||||
hash = "f5f34b1a76f65b707446cd9bee4d7cef3b6f9b5b5d8d16fcccb70dbf855c2adf";
|
||||
version = rev;
|
||||
name = "eql-git-${version}";
|
||||
};
|
||||
in
|
||||
rec {
|
||||
srcDrv = a.fetchgit {
|
||||
url = sourceInfo.url;
|
||||
sha256 = sourceInfo.hash;
|
||||
rev = sourceInfo.rev;
|
||||
};
|
||||
src = srcDrv + "/";
|
||||
|
||||
inherit (sourceInfo) name version;
|
||||
inherit buildInputs;
|
||||
|
||||
phaseNames = ["setVars" "fixPaths" "buildEQLLib" "doQMake" "doMake" "buildLibEQL" "doDeploy"];
|
||||
|
||||
setVars = a.fullDepEntry (''
|
||||
export NIX_CFLAGS_COMPILE="$NIX_CFLAGS_COMPILE -fPIC"
|
||||
'') [];
|
||||
|
||||
fixPaths = a.fullDepEntry (''
|
||||
sed -re 's@[(]in-home "gui/.command-history"[)]@(concatenate '"'"'string (ext:getenv "HOME") "/.eql-gui-command-history")@' -i gui/gui.lisp
|
||||
'') ["minInit" "doUnpack"];
|
||||
|
||||
buildEQLLib = a.fullDepEntry (''
|
||||
cd src
|
||||
ecl -shell make-eql-lib.lisp
|
||||
'') ["doUnpack" "addInputs"];
|
||||
|
||||
doQMake = a.fullDepEntry (''
|
||||
qmake
|
||||
'') ["addInputs"];
|
||||
|
||||
buildLibEQL = a.fullDepEntry (''
|
||||
sed -i eql.pro -e 's@#CONFIG += eql_dll@CONFIG += eql_dll@'
|
||||
qmake
|
||||
make
|
||||
'') ["doUnpack" "addInputs"];
|
||||
|
||||
doDeploy = a.fullDepEntry (''
|
||||
cd ..
|
||||
ensureDir $out/bin $out/lib/eql/ $out/include $out/include/gen $out/lib
|
||||
cp -r . $out/lib/eql/build-dir
|
||||
ln -s $out/lib/eql/build-dir/eql $out/bin
|
||||
ln -s $out/lib/eql/build-dir/src/*.h $out/include
|
||||
ln -s $out/lib/eql/build-dir/src/gen/*.h $out/include/gen
|
||||
mv $out/lib/eql/build-dir/my_app/libeql*.so* $out/lib
|
||||
'') ["minInit" "defEnsureDir"];
|
||||
|
||||
meta = {
|
||||
description = "Embedded Qt Lisp (ECL+Qt)";
|
||||
maintainers = with a.lib.maintainers;
|
||||
[
|
||||
raskin
|
||||
];
|
||||
platforms = with a.lib.platforms;
|
||||
linux;
|
||||
};
|
||||
passthru = {
|
||||
updateInfo = {
|
||||
downloadPage = "http://password-taxi.at/EQL";
|
||||
method = "fetchgit";
|
||||
rev = "370b7968fd73d5babc81e35913a37111a788487f";
|
||||
url = "git://gitorious.org/eql/eql";
|
||||
hash = "2370e111d86330d178f3ec95e8fed13607e51fed8859c6e95840df2a35381636";
|
||||
};
|
||||
inherit srcDrv;
|
||||
};
|
||||
}) x
|
||||
|
||||
84
pkgs/development/compilers/ghc/7.0.1.nix
Normal file
84
pkgs/development/compilers/ghc/7.0.1.nix
Normal file
@@ -0,0 +1,84 @@
|
||||
{stdenv, fetchurl, ghc, perl, gmp, ncurses}:
|
||||
|
||||
stdenv.mkDerivation rec {
|
||||
version = "7.0.1-rc1";
|
||||
|
||||
name = "ghc-${version}";
|
||||
|
||||
# TODO: Does this have to be here, or can it go to meta?
|
||||
homepage = "http://haskell.org/ghc";
|
||||
|
||||
src = fetchurl {
|
||||
url = "http://new-www.haskell.org/ghc/dist/${version}/ghc-7.0.0.20100924-src.tar.bz2";
|
||||
sha256 = "14b3cg4i805798v0rasr16nja70k68vp34qar0pv2vbwcl39apv5";
|
||||
};
|
||||
|
||||
buildInputs = [ghc perl gmp ncurses];
|
||||
|
||||
buildMK = ''
|
||||
libraries/integer-gmp_CONFIGURE_OPTS += --configure-option=--with-gmp-libraries="${gmp}/lib"
|
||||
libraries/integer-gmp_CONFIGURE_OPTS += --configure-option=--with-gmp-includes="${gmp}/include"
|
||||
'';
|
||||
|
||||
preConfigure = ''
|
||||
echo "${buildMK}" > mk/build.mk
|
||||
'';
|
||||
|
||||
configureFlags=[
|
||||
"--with-gcc=${stdenv.gcc}/bin/gcc"
|
||||
];
|
||||
|
||||
# required, because otherwise all symbols from HSffi.o are stripped, and
|
||||
# that in turn causes GHCi to abort
|
||||
stripDebugFlags=["-S" "--keep-file-symbols"];
|
||||
|
||||
meta = {
|
||||
inherit homepage;
|
||||
description = "The Glasgow Haskell Compiler";
|
||||
maintainers = [
|
||||
stdenv.lib.maintainers.marcweber
|
||||
stdenv.lib.maintainers.andres
|
||||
];
|
||||
platforms = stdenv.lib.platforms.linux;
|
||||
};
|
||||
|
||||
# TODO: requires a comment as to what it does and why it is needed.
|
||||
passthru = {
|
||||
corePackages = [
|
||||
[ "Cabal" "1.8.0.2" ]
|
||||
[ "array" "0.3.0.0" ]
|
||||
[ "base" "3.0.3.2" ]
|
||||
[ "base" "4.2.0.0" ]
|
||||
[ "bin-package-db" "0.0.0.0" ]
|
||||
[ "bytestring" "0.9.1.5" ]
|
||||
[ "containers" "0.3.0.0" ]
|
||||
[ "directory" "1.0.1.0" ]
|
||||
[ "dph-base" "0.4.0" ]
|
||||
[ "dph-par" "0.4.0" ]
|
||||
[ "dph-prim-interface" "0.4.0" ]
|
||||
[ "dph-prim-par" "0.4.0" ]
|
||||
[ "dph-prim-seq" "0.4.0" ]
|
||||
[ "dph-seq" "0.4.0" ]
|
||||
[ "extensible-exceptions" "0.1.1.1" ]
|
||||
[ "ffi" "1.0" ]
|
||||
[ "filepath" "1.1.0.3" ]
|
||||
[ "ghc" "6.12.1" ]
|
||||
[ "ghc-binary" "0.5.0.2" ]
|
||||
[ "ghc-prim" "0.2.0.0" ]
|
||||
[ "haskell98" "1.0.1.1" ]
|
||||
[ "hpc" "0.5.0.4" ]
|
||||
[ "integer-gmp" "0.2.0.0" ]
|
||||
[ "old-locale" "1.0.0.2" ]
|
||||
[ "old-time" "1.0.0.3" ]
|
||||
[ "pretty" "1.0.1.1" ]
|
||||
[ "process" "1.0.1.2" ]
|
||||
[ "random" "1.0.0.2" ]
|
||||
[ "rts" "1.0" ]
|
||||
[ "syb" "0.1.0.2" ]
|
||||
[ "template-haskell" "2.4.0.0" ]
|
||||
[ "time" "1.1.4" ]
|
||||
[ "unix" "2.4.0.0" ]
|
||||
[ "utf8-string" "0.3.4" ]
|
||||
];
|
||||
};
|
||||
}
|
||||
84
pkgs/development/compilers/ghc/head.nix
Normal file
84
pkgs/development/compilers/ghc/head.nix
Normal file
@@ -0,0 +1,84 @@
|
||||
{stdenv, fetchurl, ghc, perl, gmp, ncurses}:
|
||||
|
||||
stdenv.mkDerivation rec {
|
||||
version = "6.13.20100917";
|
||||
|
||||
name = "ghc-${version}";
|
||||
|
||||
# TODO: Does this have to be here, or can it go to meta?
|
||||
homepage = "http://haskell.org/ghc";
|
||||
|
||||
src = fetchurl {
|
||||
url = "${homepage}/dist/current/dist/${name}-src.tar.bz2";
|
||||
sha256 = "0b5pg6688yfzd5zfaffjp21y933vp94h94ds85gwi156f4g3bkij";
|
||||
};
|
||||
|
||||
buildInputs = [ghc perl gmp ncurses];
|
||||
|
||||
buildMK = ''
|
||||
libraries/integer-gmp_CONFIGURE_OPTS += --configure-option=--with-gmp-libraries="${gmp}/lib"
|
||||
libraries/integer-gmp_CONFIGURE_OPTS += --configure-option=--with-gmp-includes="${gmp}/include"
|
||||
'';
|
||||
|
||||
preConfigure = ''
|
||||
echo "${buildMK}" > mk/build.mk
|
||||
'';
|
||||
|
||||
configureFlags=[
|
||||
"--with-gcc=${stdenv.gcc}/bin/gcc"
|
||||
];
|
||||
|
||||
# required, because otherwise all symbols from HSffi.o are stripped, and
|
||||
# that in turn causes GHCi to abort
|
||||
stripDebugFlags=["-S" "--keep-file-symbols"];
|
||||
|
||||
meta = {
|
||||
inherit homepage;
|
||||
description = "The Glasgow Haskell Compiler";
|
||||
maintainers = [
|
||||
stdenv.lib.maintainers.marcweber
|
||||
stdenv.lib.maintainers.andres
|
||||
];
|
||||
platforms = stdenv.lib.platforms.linux;
|
||||
};
|
||||
|
||||
# TODO: requires a comment as to what it does and why it is needed.
|
||||
passthru = {
|
||||
corePackages = [
|
||||
[ "Cabal" "1.8.0.2" ]
|
||||
[ "array" "0.3.0.0" ]
|
||||
[ "base" "3.0.3.2" ]
|
||||
[ "base" "4.2.0.0" ]
|
||||
[ "bin-package-db" "0.0.0.0" ]
|
||||
[ "bytestring" "0.9.1.5" ]
|
||||
[ "containers" "0.3.0.0" ]
|
||||
[ "directory" "1.0.1.0" ]
|
||||
[ "dph-base" "0.4.0" ]
|
||||
[ "dph-par" "0.4.0" ]
|
||||
[ "dph-prim-interface" "0.4.0" ]
|
||||
[ "dph-prim-par" "0.4.0" ]
|
||||
[ "dph-prim-seq" "0.4.0" ]
|
||||
[ "dph-seq" "0.4.0" ]
|
||||
[ "extensible-exceptions" "0.1.1.1" ]
|
||||
[ "ffi" "1.0" ]
|
||||
[ "filepath" "1.1.0.3" ]
|
||||
[ "ghc" "6.12.1" ]
|
||||
[ "ghc-binary" "0.5.0.2" ]
|
||||
[ "ghc-prim" "0.2.0.0" ]
|
||||
[ "haskell98" "1.0.1.1" ]
|
||||
[ "hpc" "0.5.0.4" ]
|
||||
[ "integer-gmp" "0.2.0.0" ]
|
||||
[ "old-locale" "1.0.0.2" ]
|
||||
[ "old-time" "1.0.0.3" ]
|
||||
[ "pretty" "1.0.1.1" ]
|
||||
[ "process" "1.0.1.2" ]
|
||||
[ "random" "1.0.0.2" ]
|
||||
[ "rts" "1.0" ]
|
||||
[ "syb" "0.1.0.2" ]
|
||||
[ "template-haskell" "2.4.0.0" ]
|
||||
[ "time" "1.1.4" ]
|
||||
[ "unix" "2.4.0.0" ]
|
||||
[ "utf8-string" "0.3.4" ]
|
||||
];
|
||||
};
|
||||
}
|
||||
@@ -1,24 +1,15 @@
|
||||
{fetchdarcs, cabal, mtl, parsec, readline, ivor, happy}:
|
||||
{cabal, mtl, parsec, readline, ivor, epic, 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];
|
||||
version = "0.1.5";
|
||||
sha256 = "8acdfc22ba2e68b6c1832c2d5fcf11405df9416ba2c193f564b6f98710e9813e";
|
||||
propagatedBuildInputs = [mtl parsec readline ivor epic];
|
||||
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";
|
||||
license = "BSD";
|
||||
maintainers = [self.stdenv.lib.maintainers.andres];
|
||||
};
|
||||
})
|
||||
|
||||
@@ -1,586 +0,0 @@
|
||||
|
||||
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]
|
||||
@@ -1,9 +1,9 @@
|
||||
rec {
|
||||
version="1.0.41";
|
||||
name="sbcl-1.0.41";
|
||||
hash="019h0lrbd4q1f0bfwg3974pq81qcriwk5kd3v7gp1dmi5rajgnrk";
|
||||
url="http://downloads.sourceforge.net/project/sbcl/sbcl/1.0.41/sbcl-1.0.41-source.tar.bz2";
|
||||
advertisedUrl="http://downloads.sourceforge.net/project/sbcl/sbcl/1.0.41/sbcl-1.0.41-source.tar.bz2";
|
||||
version="1.0.42";
|
||||
name="sbcl-1.0.42";
|
||||
hash="0j699rb3nw7akcmpqjlzwsrc0yg6kj6nf9bzfhnw19q1m4kl4pm5";
|
||||
url="http://downloads.sourceforge.net/project/sbcl/sbcl/1.0.42/sbcl-1.0.42-source.tar.bz2";
|
||||
advertisedUrl="http://downloads.sourceforge.net/project/sbcl/sbcl/1.0.42/sbcl-1.0.42-source.tar.bz2";
|
||||
|
||||
|
||||
}
|
||||
|
||||
@@ -1,17 +1,17 @@
|
||||
{stdenv, fetchurl, pkgconfig, strategoPackages}:
|
||||
{ stdenv, fetchurl, pkgconfig, strategoPackages }:
|
||||
|
||||
stdenv.mkDerivation rec {
|
||||
name = "webdsl-9.7pre3056";
|
||||
name = "webdsl-9.7pre4168";
|
||||
|
||||
src = fetchurl {
|
||||
url = "http://hydra.nixos.org/build/71896/download/1/webdsl-9.7pre3056.tar.gz";
|
||||
sha256 = "3446b7e9dac27a9fd35541a57e961be5b74f2f9e3fb02dc14c86f945b47df045";
|
||||
url = "http://hydra.nixos.org/build/654196/download/1/${name}.tar.gz";
|
||||
sha256 = "08bec3ba02254ec7474ce70206b7be4390fe07456cfc57d927d96a21dd6dcb33";
|
||||
};
|
||||
|
||||
buildInputs = [
|
||||
pkgconfig strategoPackages.aterm strategoPackages.sdf
|
||||
strategoPackages.strategoxt strategoPackages.javafront
|
||||
];
|
||||
buildInputs =
|
||||
[ pkgconfig strategoPackages.aterm strategoPackages.sdf
|
||||
strategoPackages.strategoxt strategoPackages.javafront
|
||||
];
|
||||
|
||||
meta = {
|
||||
homepage = http://webdsl.org/;
|
||||
|
||||
Reference in New Issue
Block a user