Anthony Cowley
a523351314
redprl: patch install script shebangs
2016-09-27 18:24:06 -04:00
Kirill Boltaev
e61663a233
treewide: move to ocaml-ng system
2016-09-26 02:36:49 +03:00
Anthony Cowley
a3c26fec32
redprl: init at 2016-09-22
2016-09-23 20:37:20 -04:00
Gabriel Ebner
dd4a015aa8
eprover: 1.9 -> 1.9.1
2016-09-20 11:57:14 -04:00
Kirill Boltaev
bccd75094f
treewide: explicitly specify gtk and related package versions
2016-09-12 18:26:06 +03:00
Dan Peebles
f285ce8fed
twelf: fix emacs mode
2016-09-08 23:12:32 -04:00
Michael Raskin
b924cdefa5
tptp: take into account upstream tarball hash change; one file got renamed and some statistics in the documentation got regenerated
2016-09-08 16:49:22 +02:00
Tuomas Tynkkynen
3364230d56
Disable bunch of non-compiling packages on Darwin
...
These ones have a "Last successful build" timestamp in the 2014s or
2015s. Presumably no one will notice if we now stop building them.
softether_4_18 2015-09-20 http://hydra.nixos.org/build/39418483
lensfun 2014-09-30 http://hydra.nixos.org/build/39394104
net_snmp 2015-09-20 http://hydra.nixos.org/build/39410553
djview 2015-08-11 http://hydra.nixos.org/build/39413233
libmusicbrainz2 2015-09-20 http://hydra.nixos.org/build/39410106
fox_1_6 2014-05-07 http://hydra.nixos.org/build/39410858
libofx 2015-09-24 http://hydra.nixos.org/build/39423507
yacas 2014-09-30 http://hydra.nixos.org/build/39393150
iomelt 2014-09-30 http://hydra.nixos.org/build/39408486
softether 2015-09-20 http://hydra.nixos.org/build/39425800
mp4v2 2014-09-30 http://hydra.nixos.org/build/39421899
virtuoso7 2014-09-21 http://hydra.nixos.org/build/39415206
man_db 2015-04-23 http://hydra.nixos.org/build/39404236
libdiscid 2014-09-30 http://hydra.nixos.org/build/39412202
zabbix22.agent 2014-09-21 http://hydra.nixos.org/build/39412149
vidalia 2015-08-06 http://hydra.nixos.org/build/39411500
libmtp 2015-09-20 http://hydra.nixos.org/build/39419199
wxGTK29 2015-09-20 http://hydra.nixos.org/build/39415296
ncmpcpp 2015-11-06 http://hydra.nixos.org/build/39404455
libtorrent 2014-09-21 http://hydra.nixos.org/build/39394646
shishi 2014-03-21 http://hydra.nixos.org/build/39418874
ocaml_3_12_1 2014-09-30 http://hydra.nixos.org/build/39392996
djview4 2015-08-11 http://hydra.nixos.org/build/39427799
vimNox 2014-05-23 http://hydra.nixos.org/build/39397012
ttfautohint 2015-08-06 http://hydra.nixos.org/build/39398330
libraw 2015-09-24 http://hydra.nixos.org/build/39402271
wxGTK30 2015-09-20 http://hydra.nixos.org/build/39401871
sbcl_1_2_5 2015-09-20 http://hydra.nixos.org/build/39426091
prover9 2014-09-30 http://hydra.nixos.org/build/39406476
rcs 2015-08-25 http://hydra.nixos.org/build/39392037
gpac 2015-09-24 http://hydra.nixos.org/build/39399470
virtuoso6 2014-09-30 http://hydra.nixos.org/build/39398651
xlslib 2015-09-24 http://hydra.nixos.org/build/39410387
ucommon 2015-03-27 http://hydra.nixos.org/build/39414040
commoncpp2 2014-09-30 http://hydra.nixos.org/build/39420117
virtuoso 2014-09-21 http://hydra.nixos.org/build/39399978
miniHttpd 2014-09-30 http://hydra.nixos.org/build/39392925
mpack 2014-09-26 http://hydra.nixos.org/build/39399535
nbd 2014-09-26 http://hydra.nixos.org/build/39401367
newsbeuter-dev 2014-07-29 http://hydra.nixos.org/build/39406259
gimp_2_8 2015-09-20 http://hydra.nixos.org/build/39436271
gimp 2015-09-20 http://hydra.nixos.org/build/39435976
zabbix20.agent 2014-09-30 http://hydra.nixos.org/build/39393242
gst_all_1.gst-plugins-good 2015-09-20 http://hydra.nixos.org/build/39408506
ocaml_4_00_1 2014-09-30 http://hydra.nixos.org/build/39399526
inadyn 2014-09-30 http://hydra.nixos.org/build/39426389
gst_all_1.gst-plugins-bad 2015-09-20 http://hydra.nixos.org/build/39392970
zabbix.agent 2014-09-30 http://hydra.nixos.org/build/39421412
cmake-2_8 2015-09-24 http://hydra.nixos.org/build/39399443
liblastfm 2015-08-06 http://hydra.nixos.org/build/39421812
newsbeuter 2014-07-29 http://hydra.nixos.org/build/39396605
sdcv 2014-09-26 http://hydra.nixos.org/build/39412928
2016-09-01 20:39:33 +03:00
Robin Gloster
eddc0a5549
treewide: fix darwin builds by using getOutput
...
This fixes eval for pkgs referring to optional static output
2016-08-25 08:44:20 +00:00
Franz Pletz
df275f5b85
treewide: fix darwin builds by referring to stdenv's libc
2016-08-25 02:56:25 +02:00
Robin Gloster
bd44c7fd70
boolector: fix build with multiple outputs
2016-08-24 18:19:40 +00:00
obadz
0e8d2725dc
Merge branch 'master' into staging
2016-08-23 18:50:06 +01:00
Tuomas Tynkkynen
282277dbc8
treewide: Use more makeBinPath
2016-08-23 01:18:10 +03:00
obadz
24a9183f90
Merge branch 'hardened-stdenv' into staging
...
Closes #12895
Amazing work by @globin & @fpletz getting hardened compiler flags by
enabled default on the whole package set
2016-08-22 01:19:35 +01:00
Austin Seipp
cc7b072157
nixpkgs: abc-verifier 20160813 -> 20160818
...
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2016-08-19 01:55:13 +00:00
Robin Gloster
99cb230b47
Merge remote-tracking branch 'upstream/master' into hardened-stdenv
2016-08-14 09:09:20 +00:00
Austin Seipp
97e5b88d06
nixpkgs: abc-verifier 20150614 -> 20160813
...
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2016-08-13 17:48:42 +00:00
Robin Gloster
b7787d932e
Merge remote-tracking branch 'upstream/master' into hardened-stdenv
2016-08-12 09:46:53 +00:00
Matthew Bauer
ee63056476
aspino: patch to use c++ instead of g++
2016-08-10 22:29:18 -05:00
Robin Gloster
1b979d8384
Merge remote-tracking branch 'upstream/master' into hardened-stdenv
2016-08-03 13:34:44 +00:00
Tuomas Tynkkynen
21f17d69f6
treewide: Add lots of meta.platforms
...
Build-tested on x86_64 Linux & Mac.
2016-08-02 21:42:43 +03:00
Tuomas Tynkkynen
59ce911810
treewide: Some EOF-whitespace fixes
2016-08-02 21:17:44 +03:00
Robin Gloster
63c7b4f9a7
Merge remote-tracking branch 'upstream/master' into hardened-stdenv
2016-07-31 20:51:34 +00:00
Robert Helgesson
8878e8ec05
leo2: remove use of builderDefsPackage
( #17398 )
2016-07-31 13:57:29 +02:00
Marco Maggesi
c28eb6c2ba
Update HOL Light to version 2016-07-23.
2016-07-28 15:56:20 +02:00
Gabriel Ebner
f970bc67c7
lean: 20160117 -> 2016-07-05
...
Fixes #17260 .
2016-07-27 11:01:45 +02:00
Robin Gloster
f222d98746
Merge remote-tracking branch 'upstream/master' into hardened-stdenv
2016-07-25 12:47:13 +00:00
Gabriel Ebner
9082476478
cvc4: 1.4 -> 1.5pre-smtcomp2016
2016-07-24 13:11:17 +02:00
Gabriel Ebner
82f087944b
metis-prover: 2.3.20160102 -> 2.3.20160713
2016-07-21 18:41:26 +02:00
Robin Gloster
203846b9de
Merge remote-tracking branch 'upstream/master' into hardened-stdenv
2016-07-19 10:37:02 +00:00
Gabriel Ebner
530a9ab981
Merge remote-tracking branch 'vbgl/why3-0.87.1'
2016-07-18 13:33:50 +02:00
vbgl
d7cfdc581c
coq: 8.5pl1 -> 8.5pl2 ( #16863 )
2016-07-18 11:33:51 +02:00
Michael Raskin
61a3610853
tptp: 6.3.0 -> 6.4.0
2016-07-16 11:34:32 +02:00
Robin Gloster
5185bc1773
Merge remote-tracking branch 'upstream/master' into hardened-stdenv
2016-07-15 14:41:01 +00:00
Austin Seipp
25bf4a5634
cryptoverif: init at 1.22
...
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2016-06-28 04:37:29 +00:00
Austin Seipp
a69799c740
statverif: init at 1.86pl4
...
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2016-06-28 04:36:11 +00:00
Austin Seipp
be19637b2a
proverif: init at 1.94
...
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2016-06-28 04:36:11 +00:00
Gabriel Ebner
0a8e613cea
aspino: init at 2016-01-31
2016-06-21 13:55:28 +02:00
Gabriel Ebner
8f84a5cb08
glucose, glucose-syrup: init at 4.0
2016-06-21 13:26:51 +02:00
Gabriel Ebner
9c5588e99f
spass: 3.7 -> 3.9
2016-06-21 08:18:20 +02:00
Michael Raskin
ca495a53a5
tptp: fix hash
2016-06-20 18:38:08 +02:00
Bjørn Forsman
bd01fad0ed
Captialize meta.description of all packages
...
In line with the Nixpkgs manual.
A mechanical change, done with this command:
find pkgs -name "*.nix" | \
while read f; do \
sed -e 's/description\s*=\s*"\([a-z]\)/description = "\u\1/' -i "$f"; \
done
I manually skipped some:
* Descriptions starting with an abbreviation, a user name or package name
* Frequently generated expressions (haskell-packages.nix)
2016-06-20 13:55:52 +02:00
Gabriel Ebner
cc0b3bbcc2
minisat: support clang
2016-06-19 15:19:25 +02:00
Robin Gloster
8031cba2ab
Merge remote-tracking branch 'upstream/master' into hardened-stdenv
2016-06-10 09:27:04 +00:00
Vincent Laporte
a577b3666e
why3: 0.87.0 -> 0.87.1
2016-06-09 09:51:38 +02:00
Tuomas Tynkkynen
bac26e08db
Fix lots of fetchgit hashes (fallout from #15469 )
2016-06-03 17:17:08 +03:00
Franz Pletz
f8d481754c
Merge remote-tracking branch 'origin/master' into hardened-stdenv
2016-05-18 17:10:02 +02:00
Eelco Dolstra
7ce5d43c63
Fix some URLs that lacked a URI scheme
2016-05-09 19:35:05 +02:00
Gabriel Ebner
516f331227
minisat: migrate from builderDefsPackage to mkDerivation
2016-05-08 15:32:58 +02:00
Gabriel Ebner
3f19d757cb
veriT: disable broken static linking
2016-05-08 15:11:29 +02:00
Robin Gloster
c92bca56f8
Merge remote-tracking branch 'upstream/master' into hardened-stdenv
2016-05-02 22:58:02 +00:00
Vincent Laporte
60a7c607d1
hol-light: fix build with camlp5-6.16
2016-05-01 16:10:09 +02:00
Nikolay Amiantov
87ebab128a
replace ${stdenv.cc.cc}/lib occurences
2016-05-01 00:13:23 +03:00
Tuomas Tynkkynen
ca0e724266
otter: Mark broken
...
Build hangs an hits the hydra time limit:
http://hydra.nixos.org/build/34897110
2016-04-27 03:24:04 +03:00
Edward Tjörnhammar
f027aa2059
jonprl: corrected sha change
2016-04-26 22:23:37 +02:00
Robin Gloster
d020caa5b2
Merge remote-tracking branch 'upstream/master' into hardened-stdenv
2016-04-18 13:49:22 +00:00
Arseniy Seroka
0420a532e9
Merge pull request #14649 from vbgl/coq_8.5.1
...
Coq 8.5pl1
2016-04-13 22:16:48 +03:00
Vladimír Čunát
39ebb01d6e
Merge branch 'staging', containing closure-size #7701
2016-04-13 09:25:28 +02:00
Maarten Hoogendoorn
ec098aad41
mcrl2: 2009.01 -> 2014.09
2016-04-12 22:16:30 +02:00
Vincent Laporte
a036fda544
coq: 8.5 -> 8.5pl1
2016-04-12 19:43:11 +02:00
Vladimír Čunát
30f14243c3
Merge branch 'master' into closure-size
...
Comparison to master evaluations on Hydra:
- 1255515 for nixos
- 1255502 for nixpkgs
2016-04-10 11:17:52 +02:00
Robin Gloster
3e68106afd
Merge remote-tracking branch 'upstream/master' into hardened-stdenv
2016-04-07 21:52:26 +00:00
Vladimír Čunát
d1df28f8e5
Merge 'staging' into closure-size
...
This is mainly to get the update of bootstrap tools.
Otherwise there were mysterious segfaults:
https://github.com/NixOS/nixpkgs/pull/7701#issuecomment-203389817
2016-04-07 14:40:51 +02:00
Damien Cassou
8f7d11e39c
Merge pull request #14468 from vbgl/why3-0.87
...
why3: 0.86.3 -> 0.87.0
2016-04-05 19:15:52 +02:00
Vincent Laporte
9dfa26d2ce
why3: 0.86.3 -> 0.87.0
2016-04-05 08:09:00 +02:00
Robin Gloster
bbbaccfa68
Merge remote-tracking branch 'upstream/master' into hardened-stdenv
2016-04-04 15:24:52 +00:00
Robin Gloster
696d85a62d
Merge remote-tracking branch 'upstream/master' into hardened-stdenv
2016-04-03 11:01:57 +00:00
Gabriel Ebner
e336cd003a
picosat: enable proof output and install various utils
2016-04-02 18:45:47 +02:00
Gabriel Ebner
659c240be8
picosat: 960 -> 965
2016-04-02 18:43:32 +02:00
Vladimír Čunát
ab15a62c68
Merge branch 'master' into closure-size
...
Beware that stdenv doesn't build. It seems something more will be needed
than just resolution of merge conflicts.
2016-04-01 10:06:01 +02:00
Michael Raskin
011f69992a
satallax: 1.4 -> 2.7
2016-03-31 16:23:08 +02:00
Franz Pletz
2e08d8234e
Merge remote-tracking branch 'origin/master'
2016-03-31 10:06:30 +02:00
Michael Raskin
016d523d82
cvc4: fix the build by skipping line markers in cpp expansions during configure, helps the configure script to find Boost version
2016-03-31 01:52:33 +02:00
Robin Gloster
3f45f0948d
Merge remote-tracking branch 'upstream/master' into hardened-stdenv
2016-03-15 01:44:24 +00:00
Nicolas B. Pierron
72c6f8a140
Ensure that we can evaluate the platform attribute of ocaml packages.
2016-03-13 19:08:26 +00:00
Thomas Tuegel
3ef7671cea
ncurses: combine $lib and $out outputs
...
The $lib output refers to the terminfo database in $out, which is about
10x larger than the ncurses shared library. Splitting these outputs
saves a small amount of space for any derivations that use the terminfo
database but not the ncurses library, but we do not have evidence that
any such exist.
2016-03-08 11:35:24 -06:00
Vladimír Čunát
09af15654f
Merge master into closure-size
...
The kde-5 stuff still didn't merge well.
I hand-fixed what I saw, but there may be more problems.
2016-03-08 09:58:19 +01:00
Franz Pletz
cb3d27df93
Merge remote-tracking branch 'origin/master' into hardened-stdenv
2016-03-05 18:55:30 +01:00
Franz Pletz
aff1f4ab94
Use general hardening flag toggle lists
...
The following parameters are now available:
* hardeningDisable
To disable specific hardening flags
* hardeningEnable
To enable specific hardening flags
Only the cc-wrapper supports this right now, but these may be reused by
other wrappers, builders or setup hooks.
cc-wrapper supports the following flags:
* fortify
* stackprotector
* pie (disabled by default)
* pic
* strictoverflow
* format
* relro
* bindnow
2016-03-05 18:55:26 +01:00
Vincent Laporte
014a30da93
why3: 0.86.2 -> 0.86.3
...
And merge with ocamlPackages.why3
(the OCaml library would not work correctly if packaged separately).
2016-03-04 09:29:10 +01:00
Robin Gloster
fed49425c5
Merge remote-tracking branch 'upstream/master' into hardened-stdenv
2016-03-03 16:11:55 +00:00
Vincent Laporte
c2a2c2ecd4
ltl2ba: fix build on darwin
2016-03-03 10:24:13 +01:00
Robin Gloster
d47857c3d9
Merge remote-tracking branch 'upstream/master' into hardened-stdenv
2016-03-01 21:09:17 +00:00
Vincent Laporte
694a5ba291
eprover: fix build on Darwin
2016-02-29 15:35:40 +01:00
Robin Gloster
3477e662e6
Merge remote-tracking branch 'upstream/master' into hardened-stdenv
2016-02-27 00:08:08 +00:00
Gabriel Ebner
87b0a41ac5
isabelle: 2015 -> 2016
2016-02-23 14:19:13 +01:00
Vladimír Čunát
d039c87984
Merge branch 'master' into closure-size
2016-02-14 08:33:51 +01:00
Robin Gloster
0ea02595f7
otter: turn off format hardening
2016-02-12 13:51:05 +00:00
Robin Gloster
457f340785
prover9: turn off format hardening
2016-02-08 00:44:00 +00:00
Robin Gloster
321c57d69e
ltl2ba: turn off format hardening
2016-02-07 16:34:05 +00:00
Vladimír Čunát
ae74c356d9
Merge recent 'staging' into closure-size
...
Let's get rid of those merge conflicts.
2016-02-03 16:57:19 +01:00
Sven Keidel
ca21ae0eda
isabelle: 2014 -> 2015
...
Picked from #8510 . /cc maintainer @jwiegley.
2016-02-03 13:51:35 +01:00
Gabriel Ebner
73468cf4d4
tptp: replace use of builderDefsPackage
2016-01-29 10:33:35 +01:00
Gabriel Ebner
462958b3b7
tptp: 6.1.0 -> 6.3.0
2016-01-29 09:37:11 +01:00
John Wiegley
5009b4a8cf
coq_8_5: 8.5rc1 -> 8.5
2016-01-25 12:33:31 -08:00
Tobias Geerinckx-Rice
32d40f0f98
Remove no longer (or never) referenced patches
...
55 files changed, 6041 deletions. Tested with `nix-build -A tarball`.
2016-01-24 02:02:21 +01:00
Arseniy Seroka
f63db297d6
Merge pull request #12519 from gebner/metis-20160102
...
metis-prover: 2.3.20160101 -> 2.3.20160102
2016-01-21 18:39:57 +03:00
Ricardo M. Correia
194168b722
z3: 4.4.0 -> 4.4.1
2016-01-21 13:27:12 +01:00
Gabriel Ebner
d714963d1b
metis-prover: 2.3.20160101 -> 2.3.20160102
2016-01-21 11:26:10 +01:00
Vladimír Čunát
716aac2519
Merge branch 'staging' into closure-size
2016-01-19 09:55:31 +01:00
Gabriel Ebner
8a26d9b84f
lean: add wrapper for linja
2016-01-17 09:29:18 +01:00
Gabriel Ebner
36c430de12
lean: 20150821 -> 20160117
2016-01-17 09:29:05 +01:00
Vincent Laporte
fde89b6762
alt-ergo: also supported on Darwin
2016-01-04 17:17:44 +01:00
Gabriel Ebner
711e9e20de
metis-prover: 2.3 -> 2.3.20160101
2016-01-02 16:04:03 +01:00
Vladimír Čunát
f9f6f41bff
Merge branch 'master' into closure-size
...
TODO: there was more significant refactoring of qtbase and plasma 5.5
on master, and I'm deferring pointing to correct outputs to later.
2015-12-31 09:53:02 +01:00
John Wiegley
d80aa87b13
coqPackages_8_5.coq: 8.5b2 -> 8.5rc1
2015-12-21 16:12:43 -08:00
Luca Bruno
5b0352a6a4
Merge branch 'master' into closure-size
2015-12-11 18:31:00 +01:00
Vincent Laporte
38eb17c2e2
why3: 0.86.1 -> 0.86.2
2015-12-01 11:04:08 +01:00
Luca Bruno
920b1d3591
Merge branch 'master' into closure-size
2015-11-29 16:50:26 +01:00
Arseniy Seroka
c6932509b8
Merge pull request #11302 from fkz/sad
...
add package: system for automated deduction
2015-11-27 22:25:44 +03:00
Fabian Schmitthenner
dc164dc2ee
system for automated deduction: init at 2.3-25
2015-11-27 15:12:09 +00:00
John Wiegley
2b8ef119c5
Revert "coq: 8.5b2 -> 8.5b3"
...
This reverts commit c111b0cd4d
.
@oconnorr I will restore this once there is more ecosystem to support it.
2015-11-25 12:58:07 -08:00
Luca Bruno
a412927924
Merge remote-tracking branch 'origin/master' into closure-size
2015-11-25 21:37:30 +01:00
Joachim Fasting
4229525eac
spass: reimplement using mkDerivation
2015-11-24 14:45:15 +01:00
Joachim Fasting
0a4e12c0e2
opensmt: reimplement using mkDerivation
2015-11-24 14:45:15 +01:00
Joachim Fasting
c6d645803a
iprover: reimplement using mkDerivation
2015-11-24 14:45:15 +01:00
Joachim Fasting
a228252b69
cvc3: reimplement using mkDerivation
2015-11-24 14:45:15 +01:00
Vladimír Čunát
333d69a5f0
Merge staging into closure-size
...
The most complex problems were from dealing with switches reverted in
the meantime (gcc5, gmp6, ncurses6).
It's likely that darwin is (still) broken nontrivially.
2015-11-20 14:32:58 +01:00
Russell O'Connor
c111b0cd4d
coq: 8.5b2 -> 8.5b3
2015-11-19 00:10:22 -05:00
Marco Maggesi
a487b3326b
Update HOL Light to version 2015-11-02
2015-11-03 15:24:56 +01:00
Vladimír Čunát
fd1619cf60
yices: use correct static gmp
...
It still won't build due to trying to use /sbin/ldconfig,
but gmp-related things do seem OK.
2015-10-28 11:50:05 +01:00
Vladimír Čunát
148e03b2f1
gmp: split into multiple outputs
2015-10-28 10:15:49 +01:00
Vladimír Čunát
91407a8bdf
ncurses: split into multiple outputs
...
Some programs (e.g. tput) might better be moved somewhere else than
$dev/bin, but that can be improved later if need be.
2015-10-13 20:18:44 +02:00
Vladimír Čunát
f8c211fd2b
fontconfig: split into multiple outputs
...
Fixed all 'fontconfig}' references as well, hopefully, ugh!
2015-10-05 12:23:56 +02:00
Vladimír Čunát
5227fb1dd5
Merge commit staging+systemd into closure-size
...
Many non-conflict problems weren't (fully) resolved in this commit yet.
2015-10-03 13:33:37 +02:00
Vincent Laporte
9a1245280d
hol_light: add support for camlp5 > 6.12
2015-09-23 19:04:51 +02:00
Gabriel Ebner
5493dccfbb
metis-prover: init at 2.3
2015-09-21 21:42:20 +02:00
William A. Kennington III
773b4deb7c
Merge commit 'a6f6c0e' into master.upstream
...
This is a partial merge of staging where we have up to date binaries for
all packages.
2015-09-15 12:16:49 -07:00
Marco Maggesi
cb2a05b826
HOL Light: findlib is not necessary (nor actually used). Remove dependency.
2015-09-13 18:08:20 +02:00
Russell O'Connor
4cc5f5dbb6
coq: Add csdp dependency
...
The csdp program is invoked for some uses of Micromega tactics.
2015-09-10 11:50:38 -04:00
Austin Seipp
d8858e48e2
nixpkgs/jonprl: minor touchups
...
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2015-09-09 07:48:55 -05:00
Brian McKenna
e9bdf0fc07
JonPRL: init at 0.1.0
2015-09-09 21:23:48 +10:00
Vladimír Čunát
8f33b8cc93
mass rewrite of find parameters to cross-platform style
...
Fixes #9044 , close #9667 . Thanks to @taku0 for suggesting this solution.
Now we have no modes starting with `/` or `+`.
Rewrite the `-perm` parameters of find:
- completely safe: rewrite `/0100` and `+100` to `-0100`,
- slightly semantics-changing: rewrite `+111` to `-0100`.
I cross-verified the `find` manual pages for Linux, Darwin, FreeBSD.
2015-09-06 10:26:30 +02:00
Marco Maggesi
97b27e69c0
Update HOL Light to svn r244.
2015-09-01 16:30:27 +02:00
Austin Seipp
16b47aff4b
nixpkgs: saw-tools 0.1-20150609 -> 0.1.1-20150731
...
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2015-08-30 02:58:47 -05:00
Gabriel Ebner
0349b05695
veriT: 201410 -> 201506
2015-08-26 09:31:39 +02:00
Austin Seipp
1239465314
nixpkgs: lean 20150328 -> 20150821
...
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2015-08-21 13:57:16 -05:00
Michael Raskin
6863fde515
E prover: 1.8 -> 1.9
2015-08-08 21:01:31 +03:00
Michael Raskin
178014373e
E prover: switch to the new location
2015-07-05 18:52:42 +03:00
vbgl
5c537f3bdd
Merge pull request #8296 from vbgl/ocamlp4
...
OCaml-4.02: fix ocamlbuild rules for camlp4
2015-06-25 23:54:13 +02:00
Vincent Laporte
715f78be7e
E prover: do not build the manual
2015-06-25 23:21:25 +02:00
Vincent Laporte
1d72ce49cf
coq-8.3: fix (needs make 3)
2015-06-25 08:55:31 +02:00
Vincent Laporte
f7dc2df7c0
acgtk: fix build with OCaml 4.02
2015-06-25 08:55:30 +02:00
laMudri
723cd518b9
hol: k.8 -> k.10, closes #8477
2015-06-24 10:04:54 +02:00
Vincent Laporte
542d20384f
Isabelle: fix download URL
2015-06-21 00:45:38 +02:00
Austin Seipp
a0301e9ce2
nixpkgs: saw-tools 0.1-20150609
...
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2015-06-18 11:37:51 -05:00
Austin Seipp
2dfb657b94
nixpkgs: picosat 936 -> 960, add myself as a maintainer
...
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2015-06-14 19:48:12 -05:00
Austin Seipp
44ef5a3ab0
cvc4: regenerate ./configure on rebuild
...
Otherwise some absurd error from ./configure crops up.
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2015-06-14 19:48:11 -05:00
Austin Seipp
da76434dbd
nixpkgs: yices 2.2.1 -> 2.3.1, now with source
...
It's still under a non-commercial license, but the source build is waay
better than the binary build. Can probably work on OS X too now.
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2015-06-14 19:48:11 -05:00
Austin Seipp
3d181a3175
nixpkgs: abc-verifier 20150406 -> 20150614
...
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2015-06-14 19:48:11 -05:00
Austin Seipp
6cfc2caaeb
nixpkgs/cvc4: touchups, add myself as maintainer
...
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2015-06-14 19:48:11 -05:00
Austin Seipp
da6eec001a
nixpkgs: z3 4.3.2 -> 4.4.0
...
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2015-06-11 22:10:56 -05:00
Marco
3af4c7065d
Update HOL Light to svn r232 (2015-05-31)
2015-06-03 11:17:39 +02:00
Vincent Laporte
28bfbb5562
why3: update from 0.85 to 0.86.1
2015-06-01 05:57:19 +02:00
Tobias Geerinckx-Rice
158e1cfdd0
Don't use "with licenses;" for single licences
...
And don't use square brackets on such lines.
2015-05-28 19:20:29 +02:00
Vincent Laporte
9f1eb28a20
Adds gappa 1.2.0
...
Gappa is a tool intended to help verifying and formally proving
properties on numerical programs dealing with floating-point or
fixed-point arithmetic.
Homepage: http://gappa.gforge.inria.fr/
2015-05-25 19:32:09 +02:00
Pascal Wittmann
c944422863
lean: fixed build
2015-05-16 12:12:58 +02:00
Aistis Raulinaitis
a5a740a17a
z3 opt
2015-05-08 23:45:07 -07:00
Vladimír Čunát
3b9ef2c71b
fix "libc}/lib" and similar references
...
Done mostly without any verification.
I didn't bother with libc}/include, as the path is still correct.
2015-05-05 11:52:08 +02:00
Joachim Fasting
bf7ad2d84f
meta.description fixups
...
Mostly scripted substitutions with a couple of subjective enhancements.
2015-04-30 18:17:42 +02:00
John Wiegley
9402a56620
coq_8_5: New expression
2015-04-26 22:29:15 -05:00
Vincent Laporte
4b9c90c64e
coq: update from 8.4pl5 to 8.4pl6
2015-04-15 07:18:08 +02:00
Austin Seipp
31f4c0c7d1
nixpkgs: abc-verifier 20140509 -> 20150406
...
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2015-04-06 07:57:27 -05:00
lethalman
b4824ffc5d
Merge pull request #7103 from gebner/verit
...
Add veriT, an SMT solver.
2015-03-31 12:31:26 +02:00
Gabriel Ebner
20428cd90f
Add veriT.
2015-03-31 09:14:38 +02:00
Ben Darwin
54dab782be
twelf: fix by actually including the Twelf SML heap image in the package and referencing the SML interpreter so the smlnj package won't be gc'd
2015-03-31 01:11:57 -04:00
Austin Seipp
a6813ca62d
nixpkgs: add lean-20150328, a theorem prover.
...
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2015-03-28 01:47:39 -05:00
Austin Seipp
75ab87edc8
nixpkgs: z3 is now MIT licensed.
...
It's also been moved to GitHub, meaning we can avoid some of the
hackiness in the original expression. This updates the Git revision, but
only so that it contains the proper license (it's otherwise equivalent
to Z3 v4.3.2)
Also, make sure the python API .py files exist besides the .pyc files.
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2015-03-28 01:04:06 -05:00
Eric Seidel
eff828a275
z3: copy all headers into nix store
2015-03-26 13:19:41 -07:00
Ben Darwin
172167c937
new package: abella 2.0.2
2015-03-24 00:54:03 -04:00
Marco
5f6e6b1661
Update HOL Light to r218
2015-02-17 10:23:51 +01:00
Vladimír Čunát
dbae4f109f
Merge branch 'master' into staging
...
Conflicts (relatively simple):
pkgs/applications/audio/spotify/default.nix
pkgs/build-support/cc-wrapper/default.nix
pkgs/development/compilers/cryptol/1.8.x.nix
2015-01-31 19:34:57 +01:00
Vincent Laporte
58297aa1e7
Why3: build also the Coq tactic.
2015-01-29 08:43:15 +01:00
Austin Seipp
d1b06927bc
nixpkgs: z3 4.3.1 -> 4.3.2
...
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2015-01-23 11:00:55 -06:00
Eric Seidel
f3c6827373
rename all occurrences of stdenv.cc.gcc to stdenv.cc.cc
2015-01-14 20:27:55 -08:00
Pavan Rikhi
56ea7c4128
matita_130312: mark as broken
2015-01-07 02:15:26 -05:00
John Wiegley
c4190b4894
abc: export buildFlags in the preBuild
2015-01-03 07:35:36 -05:00
Vincent Laporte
06fea66e7c
alt-ergo: update from 0.95.2 to 0.99.1
2014-12-31 15:48:39 +01:00
John Wiegley
28b6fb61e6
Change occurrences of gcc to the more general cc
...
This is done for the sake of Yosemite, which does not have gcc, and yet
this change is also compatible with Linux.
2014-12-26 11:06:21 -06:00
Pascal Wittmann
f94580da69
Fix license attribute of many bsd-like licensed packages
2014-12-21 00:00:35 +01:00
John Wiegley
d15cd4875f
coq_HEAD: update to latest Git version
2014-12-19 13:58:07 -06:00
John Wiegley
1825255272
coq_HEAD: update
2014-11-17 17:29:42 -06:00
Vincent Laporte
8227297567
hol_light: update from 199 to 205
2014-11-17 06:53:45 +00:00
Vincent Laporte
fbbd88017f
zarith: propagate build input gmp
2014-11-07 09:50:39 +00:00
Vincent Laporte
3d049938c8
Adds some “branch” meta-data
2014-11-06 19:40:50 +00:00
Mateusz Kowalczyk
007f80c1d0
Turn more licenses into lib.licenses style
...
Should eval cleanly, as far as -A tarball tells me.
Relevant: issue #2999 , issue #739
2014-11-06 00:48:16 +00:00
Peter Simons
b5fed52c43
Merge pull request #4238 from wkennington/master.boost
...
Make boost 156 the default
2014-11-03 23:03:01 +01:00
John Wiegley
d4c3e454a2
coq_HEAD: update to latest commit
2014-11-03 15:27:32 -06:00
John Wiegley
2b9e43b513
coq: 8.4pl4 -> 8.4pl5
2014-11-03 10:49:38 -06:00
William A. Kennington III
aa3e800be7
boost: Remove boost.lib
2014-11-02 17:22:27 -08:00
Jiri Marsik
ceba23605c
Added acgtk-1.1
2014-10-28 14:06:21 +01:00
Vincent Laporte
fe1d8d0015
cvc4: new derivation
...
CVC4 is an efficient open-source automatic theorem prover for
satisfiability modulo theories (SMT) problems.
Homepage: http://cvc4.cs.nyu.edu/web/
2014-10-12 16:21:02 +02:00
Vincent Laporte
531b44562a
why3: update from 0.83 to 0.85
2014-10-12 16:21:02 +02:00
John Wiegley
e73aefcf93
coq_HEAD: Update
2014-10-09 14:52:35 -05:00
Mateusz Kowalczyk
3d26ea99dc
Merge pull request #4342 from vbgl/camlp5-6.12
...
Camlp5: update to 6.12; hol-light: update to r199
2014-10-03 18:36:06 +01:00
John Wiegley
10e215a3ae
isabelle: Version 2014 building on Linux and Darwin
2014-09-30 23:15:31 -05:00
Vincent Laporte
c260abbff8
hol_light: update to r199
...
And adds compatibility with camlp5-6.12
2014-10-01 00:44:15 +01:00
John Wiegley
57b292fb1b
isabelle: Another Linux hash change?
2014-09-30 16:44:15 -05:00
John Wiegley
5a7ce1185b
isabelle: Remove Linux patches (is this correct?)
2014-09-30 16:41:47 -05:00
John Wiegley
8d9cd1557b
isabelle: Correct the 2014 sha value for Linux
2014-09-30 16:15:34 -05:00