Merge branch 'master' into staging-next
Trivial conflict in release notes, except that the xml/docbook parts are horrible for (semi-)automatic conflict resolution. Fortunately that's generated anyway.
This commit is contained in:
commit
411405c9f6
163 changed files with 1344 additions and 575 deletions
|
@ -28,13 +28,13 @@ mkShell {
|
|||
packages = [
|
||||
(with dotnetCorePackages; combinePackages [
|
||||
sdk_3_1
|
||||
sdk_5_0
|
||||
sdk_6_0
|
||||
])
|
||||
];
|
||||
}
|
||||
```
|
||||
|
||||
This will produce a dotnet installation that has the dotnet 3.1, 3.0, and 2.1 sdk. The first sdk listed will have it's cli utility present in the resulting environment. Example info output:
|
||||
This will produce a dotnet installation that has the dotnet 3.1 6.0 sdk. The first sdk listed will have it's cli utility present in the resulting environment. Example info output:
|
||||
|
||||
```ShellSession
|
||||
$ dotnet --info
|
||||
|
@ -120,7 +120,7 @@ in buildDotnetModule rec {
|
|||
projectReferences = [ referencedProject ]; # `referencedProject` must contain `nupkg` in the folder structure.
|
||||
|
||||
dotnet-sdk = dotnetCorePackages.sdk_3_1;
|
||||
dotnet-runtime = dotnetCorePackages.net_5_0;
|
||||
dotnet-runtime = dotnetCorePackages.net_6_0;
|
||||
|
||||
executables = [ "foo" ]; # This wraps "$out/lib/$pname/foo" to `$out/bin/foo`.
|
||||
executables = []; # Don't install any executables.
|
||||
|
|
|
@ -715,7 +715,12 @@ in mkLicense lset) ({
|
|||
|
||||
ncsa = {
|
||||
spdxId = "NCSA";
|
||||
fullName = "University of Illinois/NCSA Open Source License";
|
||||
fullName = "University of Illinois/NCSA Open Source License";
|
||||
};
|
||||
|
||||
nlpl = {
|
||||
spdxId = "NLPL";
|
||||
fullName = "No Limit Public License";
|
||||
};
|
||||
|
||||
nposl3 = {
|
||||
|
|
|
@ -12263,6 +12263,12 @@
|
|||
githubId = 710906;
|
||||
name = "Roel van Dijk";
|
||||
};
|
||||
roman = {
|
||||
email = "open-source@roman-gonzalez.info";
|
||||
github = "roman";
|
||||
githubId = 7335;
|
||||
name = "Roman Gonzalez";
|
||||
};
|
||||
romildo = {
|
||||
email = "malaquias@gmail.com";
|
||||
github = "romildo";
|
||||
|
|
|
@ -65,6 +65,7 @@ luaevent,,,,,,
|
|||
luaexpat,,,,1.4.1-1,,arobyn flosse
|
||||
luaffi,,,http://luarocks.org/dev,,,
|
||||
luafilesystem,,,,1.8.0-1,,flosse
|
||||
lualdap,,,,,,aanderse
|
||||
lualogging,,,,,,
|
||||
luaossl,,,,,5.1,
|
||||
luaposix,,,,34.1.1-1,,vyp lblasc
|
||||
|
|
|
|
@ -61,6 +61,13 @@
|
|||
<link linkend="opt-services.printing.cups-pdf.enable">services.printing.cups-pdf</link>.
|
||||
</para>
|
||||
</listitem>
|
||||
<listitem>
|
||||
<para>
|
||||
<link xlink:href="https://www.magicbug.co.uk/cloudlog/">Cloudlog</link>,
|
||||
a web-based Amateur Radio logging application. Available as
|
||||
<link linkend="opt-services.cloudlog.enable">services.cloudlog</link>.
|
||||
</para>
|
||||
</listitem>
|
||||
<listitem>
|
||||
<para>
|
||||
<link xlink:href="https://github.com/junegunn/fzf">fzf</link>,
|
||||
|
@ -378,6 +385,13 @@
|
|||
<literal>freetype</literal> and others.
|
||||
</para>
|
||||
</listitem>
|
||||
<listitem>
|
||||
<para>
|
||||
.NET 5.0 was removed due to being end-of-life, use a newer,
|
||||
supported .NET version -
|
||||
https://dotnet.microsoft.com/en-us/platform/support/policy/dotnet-core
|
||||
</para>
|
||||
</listitem>
|
||||
<listitem>
|
||||
<para>
|
||||
The iputils package, which is installed by default, no longer
|
||||
|
|
|
@ -24,6 +24,8 @@ In addition to numerous new and upgraded packages, this release has the followin
|
|||
|
||||
- [cups-pdf-to-pdf](https://github.com/alexivkin/CUPS-PDF-to-PDF), a pdf-generating cups backend based on [cups-pdf](https://www.cups-pdf.de/). Available as [services.printing.cups-pdf](#opt-services.printing.cups-pdf.enable).
|
||||
|
||||
- [Cloudlog](https://www.magicbug.co.uk/cloudlog/), a web-based Amateur Radio logging application. Available as [services.cloudlog](#opt-services.cloudlog.enable).
|
||||
|
||||
- [fzf](https://github.com/junegunn/fzf), a command line fuzzyfinder. Available as [programs.fzf](#opt-programs.fzf.fuzzyCompletion).
|
||||
|
||||
- [gmediarender](https://github.com/hzeller/gmrender-resurrect), a simple, headless UPnP/DLNA renderer. Available as [services.gmediarender](options.html#opt-services.gmediarender.enable).
|
||||
|
@ -93,6 +95,8 @@ In addition to numerous new and upgraded packages, this release has the followin
|
|||
|
||||
- Deprecated `xlibsWrapper` transitional package has been removed in favour of direct use of its constitutents: `xorg.libX11`, `freetype` and others.
|
||||
|
||||
- .NET 5.0 was removed due to being end-of-life, use a newer, supported .NET version - https://dotnet.microsoft.com/en-us/platform/support/policy/dotnet-core
|
||||
|
||||
- The iputils package, which is installed by default, no longer provides the
|
||||
`ninfod`, `rarpd` and `rdisc` tools. See
|
||||
[upstream's release notes](https://github.com/iputils/iputils/releases/tag/20221126)
|
||||
|
|
|
@ -1119,6 +1119,7 @@
|
|||
./services/web-apps/bookstack.nix
|
||||
./services/web-apps/calibre-web.nix
|
||||
./services/web-apps/changedetection-io.nix
|
||||
./services/web-apps/cloudlog.nix
|
||||
./services/web-apps/code-server.nix
|
||||
./services/web-apps/convos.nix
|
||||
./services/web-apps/dex.nix
|
||||
|
|
502
nixos/modules/services/web-apps/cloudlog.nix
Normal file
502
nixos/modules/services/web-apps/cloudlog.nix
Normal file
|
@ -0,0 +1,502 @@
|
|||
{ config, pkgs, lib, ... }:
|
||||
|
||||
with lib;
|
||||
|
||||
let
|
||||
cfg = config.services.cloudlog;
|
||||
dbFile = let
|
||||
password = if cfg.database.createLocally
|
||||
then "''"
|
||||
else "trim(file_get_contents('${cfg.database.passwordFile}'))";
|
||||
in pkgs.writeText "database.php" ''
|
||||
<?php
|
||||
defined('BASEPATH') OR exit('No direct script access allowed');
|
||||
$active_group = 'default';
|
||||
$query_builder = TRUE;
|
||||
$db['default'] = array(
|
||||
'dsn' => "",
|
||||
'hostname' => '${cfg.database.host}',
|
||||
'username' => '${cfg.database.user}',
|
||||
'password' => ${password},
|
||||
'database' => '${cfg.database.name}',
|
||||
'dbdriver' => 'mysqli',
|
||||
'dbprefix' => "",
|
||||
'pconnect' => TRUE,
|
||||
'db_debug' => (ENVIRONMENT !== 'production'),
|
||||
'cache_on' => FALSE,
|
||||
'cachedir' => "",
|
||||
'char_set' => 'utf8mb4',
|
||||
'dbcollat' => 'utf8mb4_general_ci',
|
||||
'swap_pre' => "",
|
||||
'encrypt' => FALSE,
|
||||
'compress' => FALSE,
|
||||
'stricton' => FALSE,
|
||||
'failover' => array(),
|
||||
'save_queries' => TRUE
|
||||
);
|
||||
'';
|
||||
configFile = pkgs.writeText "config.php" ''
|
||||
${strings.fileContents "${pkgs.cloudlog}/install/config/config.php"}
|
||||
$config['datadir'] = "${cfg.dataDir}/";
|
||||
$config['base_url'] = "${cfg.baseUrl}";
|
||||
${cfg.extraConfig}
|
||||
'';
|
||||
package = pkgs.stdenv.mkDerivation rec {
|
||||
pname = "cloudlog";
|
||||
version = src.version;
|
||||
src = pkgs.cloudlog;
|
||||
installPhase = ''
|
||||
mkdir -p $out
|
||||
cp -r * $out/
|
||||
|
||||
ln -s ${configFile} $out/application/config/config.php
|
||||
ln -s ${dbFile} $out/application/config/database.php
|
||||
|
||||
# link writable directories
|
||||
for directory in updates uploads backup logbook; do
|
||||
rm -rf $out/$directory
|
||||
ln -s ${cfg.dataDir}/$directory $out/$directory
|
||||
done
|
||||
|
||||
# link writable asset files
|
||||
for asset in dok sota wwff; do
|
||||
rm -rf $out/assets/json/$asset.txt
|
||||
ln -s ${cfg.dataDir}/assets/json/$asset.txt $out/assets/json/$asset.txt
|
||||
done
|
||||
'';
|
||||
};
|
||||
in
|
||||
{
|
||||
options.services.cloudlog = with types; {
|
||||
enable = mkEnableOption (mdDoc "Whether to enable Cloudlog.");
|
||||
dataDir = mkOption {
|
||||
type = str;
|
||||
default = "/var/lib/cloudlog";
|
||||
description = mdDoc "Cloudlog data directory.";
|
||||
};
|
||||
baseUrl = mkOption {
|
||||
type = str;
|
||||
default = "http://localhost";
|
||||
description = mdDoc "Cloudlog base URL";
|
||||
};
|
||||
user = mkOption {
|
||||
type = str;
|
||||
default = "cloudlog";
|
||||
description = mdDoc "User account under which Cloudlog runs.";
|
||||
};
|
||||
database = {
|
||||
createLocally = mkOption {
|
||||
type = types.bool;
|
||||
default = true;
|
||||
description = lib.mdDoc "Create the database and database user locally.";
|
||||
};
|
||||
host = mkOption {
|
||||
type = str;
|
||||
description = mdDoc "MySQL database host";
|
||||
default = "localhost";
|
||||
};
|
||||
name = mkOption {
|
||||
type = str;
|
||||
description = mdDoc "MySQL database name.";
|
||||
default = "cloudlog";
|
||||
};
|
||||
user = mkOption {
|
||||
type = str;
|
||||
description = mdDoc "MySQL user name.";
|
||||
default = "cloudlog";
|
||||
};
|
||||
passwordFile = mkOption {
|
||||
type = nullOr str;
|
||||
description = mdDoc "MySQL user password file.";
|
||||
default = null;
|
||||
};
|
||||
};
|
||||
poolConfig = mkOption {
|
||||
type = attrsOf (oneOf [ str int bool ]);
|
||||
default = {
|
||||
"pm" = "dynamic";
|
||||
"pm.max_children" = 32;
|
||||
"pm.start_servers" = 2;
|
||||
"pm.min_spare_servers" = 2;
|
||||
"pm.max_spare_servers" = 4;
|
||||
"pm.max_requests" = 500;
|
||||
};
|
||||
description = mdDoc ''
|
||||
Options for Cloudlog's PHP-FPM pool.
|
||||
'';
|
||||
};
|
||||
virtualHost = mkOption {
|
||||
type = nullOr str;
|
||||
default = "localhost";
|
||||
description = mdDoc ''
|
||||
Name of the nginx virtualhost to use and setup. If null, do not setup
|
||||
any virtualhost.
|
||||
'';
|
||||
};
|
||||
extraConfig = mkOption {
|
||||
description = mdDoc ''
|
||||
Any additional text to be appended to the config.php
|
||||
configuration file. This is a PHP script. For configuration
|
||||
settings, see <https://github.com/magicbug/Cloudlog/wiki/Cloudlog.php-Configuration-File>.
|
||||
'';
|
||||
default = "";
|
||||
type = str;
|
||||
example = ''
|
||||
$config['show_time'] = TRUE;
|
||||
'';
|
||||
};
|
||||
upload-lotw = {
|
||||
enable = mkOption {
|
||||
type = bool;
|
||||
default = true;
|
||||
description = mdDoc ''
|
||||
Whether to periodically upload logs to LoTW. If enabled, a systemd
|
||||
timer will run the log upload task as specified by the interval
|
||||
option.
|
||||
'';
|
||||
};
|
||||
interval = mkOption {
|
||||
type = str;
|
||||
default = "daily";
|
||||
description = mdDoc ''
|
||||
Specification (in the format described by systemd.time(7)) of the
|
||||
time at which the LoTW upload will occur.
|
||||
'';
|
||||
};
|
||||
};
|
||||
upload-clublog = {
|
||||
enable = mkOption {
|
||||
type = bool;
|
||||
default = true;
|
||||
description = mdDoc ''
|
||||
Whether to periodically upload logs to Clublog. If enabled, a systemd
|
||||
timer will run the log upload task as specified by the interval option.
|
||||
'';
|
||||
};
|
||||
interval = mkOption {
|
||||
type = str;
|
||||
default = "daily";
|
||||
description = mdDoc ''
|
||||
Specification (in the format described by systemd.time(7)) of the time
|
||||
at which the Clublog upload will occur.
|
||||
'';
|
||||
};
|
||||
};
|
||||
update-lotw-users = {
|
||||
enable = mkOption {
|
||||
type = bool;
|
||||
default = true;
|
||||
description = mdDoc ''
|
||||
Whether to periodically update the list of LoTW users. If enabled, a
|
||||
systemd timer will run the update task as specified by the interval
|
||||
option.
|
||||
'';
|
||||
};
|
||||
interval = mkOption {
|
||||
type = str;
|
||||
default = "weekly";
|
||||
description = mdDoc ''
|
||||
Specification (in the format described by systemd.time(7)) of the
|
||||
time at which the LoTW user update will occur.
|
||||
'';
|
||||
};
|
||||
};
|
||||
update-dok = {
|
||||
enable = mkOption {
|
||||
type = bool;
|
||||
default = true;
|
||||
description = mdDoc ''
|
||||
Whether to periodically update the DOK resource file. If enabled, a
|
||||
systemd timer will run the update task as specified by the interval option.
|
||||
'';
|
||||
};
|
||||
interval = mkOption {
|
||||
type = str;
|
||||
default = "monthly";
|
||||
description = mdDoc ''
|
||||
Specification (in the format described by systemd.time(7)) of the
|
||||
time at which the DOK update will occur.
|
||||
'';
|
||||
};
|
||||
};
|
||||
update-clublog-scp = {
|
||||
enable = mkOption {
|
||||
type = bool;
|
||||
default = true;
|
||||
description = mdDoc ''
|
||||
Whether to periodically update the Clublog SCP database. If enabled,
|
||||
a systemd timer will run the update task as specified by the interval
|
||||
option.
|
||||
'';
|
||||
};
|
||||
interval = mkOption {
|
||||
type = str;
|
||||
default = "monthly";
|
||||
description = mdDoc ''
|
||||
Specification (in the format described by systemd.time(7)) of the time
|
||||
at which the Clublog SCP update will occur.
|
||||
'';
|
||||
};
|
||||
};
|
||||
update-wwff = {
|
||||
enable = mkOption {
|
||||
type = bool;
|
||||
default = true;
|
||||
description = mdDoc ''
|
||||
Whether to periodically update the WWFF database. If enabled, a
|
||||
systemd timer will run the update task as specified by the interval
|
||||
option.
|
||||
'';
|
||||
};
|
||||
interval = mkOption {
|
||||
type = str;
|
||||
default = "monthly";
|
||||
description = mdDoc ''
|
||||
Specification (in the format described by systemd.time(7)) of the time
|
||||
at which the WWFF update will occur.
|
||||
'';
|
||||
};
|
||||
};
|
||||
upload-qrz = {
|
||||
enable = mkOption {
|
||||
type = bool;
|
||||
default = true;
|
||||
description = mdDoc ''
|
||||
Whether to periodically upload logs to QRZ. If enabled, a systemd
|
||||
timer will run the update task as specified by the interval option.
|
||||
'';
|
||||
};
|
||||
interval = mkOption {
|
||||
type = str;
|
||||
default = "daily";
|
||||
description = mdDoc ''
|
||||
Specification (in the format described by systemd.time(7)) of the
|
||||
time at which the QRZ upload will occur.
|
||||
'';
|
||||
};
|
||||
};
|
||||
update-sota = {
|
||||
enable = mkOption {
|
||||
type = bool;
|
||||
default = true;
|
||||
description = mdDoc ''
|
||||
Whether to periodically update the SOTA database. If enabled, a
|
||||
systemd timer will run the update task as specified by the interval option.
|
||||
'';
|
||||
};
|
||||
interval = mkOption {
|
||||
type = str;
|
||||
default = "monthly";
|
||||
description = mdDoc ''
|
||||
Specification (in the format described by systemd.time(7)) of the time
|
||||
at which the SOTA update will occur.
|
||||
'';
|
||||
};
|
||||
};
|
||||
};
|
||||
config = mkIf cfg.enable {
|
||||
|
||||
assertions = [
|
||||
{
|
||||
assertion = cfg.database.createLocally -> cfg.database.passwordFile == null;
|
||||
message = "services.cloudlog.database.passwordFile cannot be specified if services.cloudlog.database.createLocally is set to true.";
|
||||
}
|
||||
];
|
||||
|
||||
services.phpfpm = {
|
||||
pools.cloudlog = {
|
||||
inherit (cfg) user;
|
||||
group = config.services.nginx.group;
|
||||
settings = {
|
||||
"listen.owner" = config.services.nginx.user;
|
||||
"listen.group" = config.services.nginx.group;
|
||||
} // cfg.poolConfig;
|
||||
};
|
||||
};
|
||||
|
||||
services.nginx = mkIf (cfg.virtualHost != null) {
|
||||
enable = true;
|
||||
virtualHosts = {
|
||||
"${cfg.virtualHost}" = {
|
||||
root = "${package}";
|
||||
locations."/".tryFiles = "$uri /index.php$is_args$args";
|
||||
locations."~ ^/index.php(/|$)".extraConfig = ''
|
||||
include ${config.services.nginx.package}/conf/fastcgi_params;
|
||||
include ${pkgs.nginx}/conf/fastcgi.conf;
|
||||
fastcgi_split_path_info ^(.+\.php)(.+)$;
|
||||
fastcgi_pass unix:${config.services.phpfpm.pools.cloudlog.socket};
|
||||
fastcgi_param SCRIPT_FILENAME $document_root$fastcgi_script_name;
|
||||
'';
|
||||
};
|
||||
};
|
||||
};
|
||||
|
||||
services.mysql = mkIf cfg.database.createLocally {
|
||||
enable = true;
|
||||
ensureDatabases = [ cfg.database.name ];
|
||||
ensureUsers = [{
|
||||
name = cfg.database.user;
|
||||
ensurePermissions = {
|
||||
"${cfg.database.name}.*" = "ALL PRIVILEGES";
|
||||
};
|
||||
}];
|
||||
};
|
||||
|
||||
systemd = {
|
||||
services = {
|
||||
cloudlog-setup-database = mkIf cfg.database.createLocally {
|
||||
description = "Set up cloudlog database";
|
||||
serviceConfig = {
|
||||
Type = "oneshot";
|
||||
RemainAfterExit = true;
|
||||
};
|
||||
wantedBy = [ "phpfpm-cloudlog.service" ];
|
||||
after = [ "mysql.service" ];
|
||||
script = let
|
||||
mysql = "${config.services.mysql.package}/bin/mysql";
|
||||
in ''
|
||||
if [ ! -f ${cfg.dataDir}/.dbexists ]; then
|
||||
${mysql} ${cfg.database.name} < ${pkgs.cloudlog}/install/assets/install.sql
|
||||
touch ${cfg.dataDir}/.dbexists
|
||||
fi
|
||||
'';
|
||||
};
|
||||
cloudlog-upload-lotw = {
|
||||
description = "Upload QSOs to LoTW if certs have been provided";
|
||||
enable = cfg.upload-lotw.enable;
|
||||
script = "${pkgs.curl}/bin/curl -s ${cfg.baseUrl}/lotw/lotw_upload";
|
||||
};
|
||||
cloudlog-update-lotw-users = {
|
||||
description = "Update LOTW Users Database";
|
||||
enable = cfg.update-lotw-users.enable;
|
||||
script = "${pkgs.curl}/bin/curl -s ${cfg.baseUrl}/lotw/load_users";
|
||||
};
|
||||
cloudlog-update-dok = {
|
||||
description = "Update DOK File for autocomplete";
|
||||
enable = cfg.update-dok.enable;
|
||||
script = "${pkgs.curl}/bin/curl -s ${cfg.baseUrl}/update/update_dok";
|
||||
};
|
||||
cloudlog-update-clublog-scp = {
|
||||
description = "Update Clublog SCP Database File";
|
||||
enable = cfg.update-clublog-scp.enable;
|
||||
script = "${pkgs.curl}/bin/curl -s ${cfg.baseUrl}/update/update_clublog_scp";
|
||||
};
|
||||
cloudlog-update-wwff = {
|
||||
description = "Update WWFF File for autocomplete";
|
||||
enable = cfg.update-wwff.enable;
|
||||
script = "${pkgs.curl}/bin/curl -s ${cfg.baseUrl}/update/update_wwff";
|
||||
};
|
||||
cloudlog-upload-qrz = {
|
||||
description = "Upload QSOs to QRZ Logbook";
|
||||
enable = cfg.upload-qrz.enable;
|
||||
script = "${pkgs.curl}/bin/curl -s ${cfg.baseUrl}/qrz/upload";
|
||||
};
|
||||
cloudlog-update-sota = {
|
||||
description = "Update SOTA File for autocomplete";
|
||||
enable = cfg.update-sota.enable;
|
||||
script = "${pkgs.curl}/bin/curl -s ${cfg.baseUrl}/update/update_sota";
|
||||
};
|
||||
};
|
||||
timers = {
|
||||
cloudlog-upload-lotw = {
|
||||
enable = cfg.upload-lotw.enable;
|
||||
wantedBy = [ "timers.target" ];
|
||||
partOf = [ "cloudlog-upload-lotw.service" ];
|
||||
after = [ "phpfpm-cloudlog.service" ];
|
||||
timerConfig = {
|
||||
OnCalendar = cfg.upload-lotw.interval;
|
||||
Persistent = true;
|
||||
};
|
||||
};
|
||||
cloudlog-upload-clublog = {
|
||||
enable = cfg.upload-clublog.enable;
|
||||
wantedBy = [ "timers.target" ];
|
||||
partOf = [ "cloudlog-upload-clublog.service" ];
|
||||
after = [ "phpfpm-cloudlog.service" ];
|
||||
timerConfig = {
|
||||
OnCalendar = cfg.upload-clublog.interval;
|
||||
Persistent = true;
|
||||
};
|
||||
};
|
||||
cloudlog-update-lotw-users = {
|
||||
enable = cfg.update-lotw-users.enable;
|
||||
wantedBy = [ "timers.target" ];
|
||||
partOf = [ "cloudlog-update-lotw-users.service" ];
|
||||
after = [ "phpfpm-cloudlog.service" ];
|
||||
timerConfig = {
|
||||
OnCalendar = cfg.update-lotw-users.interval;
|
||||
Persistent = true;
|
||||
};
|
||||
};
|
||||
cloudlog-update-dok = {
|
||||
enable = cfg.update-dok.enable;
|
||||
wantedBy = [ "timers.target" ];
|
||||
partOf = [ "cloudlog-update-dok.service" ];
|
||||
after = [ "phpfpm-cloudlog.service" ];
|
||||
timerConfig = {
|
||||
OnCalendar = cfg.update-dok.interval;
|
||||
Persistent = true;
|
||||
};
|
||||
};
|
||||
cloudlog-update-clublog-scp = {
|
||||
enable = cfg.update-clublog-scp.enable;
|
||||
wantedBy = [ "timers.target" ];
|
||||
partOf = [ "cloudlog-update-clublog-scp.service" ];
|
||||
after = [ "phpfpm-cloudlog.service" ];
|
||||
timerConfig = {
|
||||
OnCalendar = cfg.update-clublog-scp.interval;
|
||||
Persistent = true;
|
||||
};
|
||||
};
|
||||
cloudlog-update-wwff = {
|
||||
enable = cfg.update-wwff.enable;
|
||||
wantedBy = [ "timers.target" ];
|
||||
partOf = [ "cloudlog-update-wwff.service" ];
|
||||
after = [ "phpfpm-cloudlog.service" ];
|
||||
timerConfig = {
|
||||
OnCalendar = cfg.update-wwff.interval;
|
||||
Persistent = true;
|
||||
};
|
||||
};
|
||||
cloudlog-upload-qrz = {
|
||||
enable = cfg.upload-qrz.enable;
|
||||
wantedBy = [ "timers.target" ];
|
||||
partOf = [ "cloudlog-upload-qrz.service" ];
|
||||
after = [ "phpfpm-cloudlog.service" ];
|
||||
timerConfig = {
|
||||
OnCalendar = cfg.upload-qrz.interval;
|
||||
Persistent = true;
|
||||
};
|
||||
};
|
||||
cloudlog-update-sota = {
|
||||
enable = cfg.update-sota.enable;
|
||||
wantedBy = [ "timers.target" ];
|
||||
partOf = [ "cloudlog-update-sota.service" ];
|
||||
after = [ "phpfpm-cloudlog.service" ];
|
||||
timerConfig = {
|
||||
OnCalendar = cfg.update-sota.interval;
|
||||
Persistent = true;
|
||||
};
|
||||
};
|
||||
};
|
||||
tmpfiles.rules = let
|
||||
group = config.services.nginx.group;
|
||||
in [
|
||||
"d ${cfg.dataDir} 0750 ${cfg.user} ${group} - -"
|
||||
"d ${cfg.dataDir}/updates 0750 ${cfg.user} ${group} - -"
|
||||
"d ${cfg.dataDir}/uploads 0750 ${cfg.user} ${group} - -"
|
||||
"d ${cfg.dataDir}/backup 0750 ${cfg.user} ${group} - -"
|
||||
"d ${cfg.dataDir}/logbook 0750 ${cfg.user} ${group} - -"
|
||||
"d ${cfg.dataDir}/assets/json 0750 ${cfg.user} ${group} - -"
|
||||
"d ${cfg.dataDir}/assets/qslcard 0750 ${cfg.user} ${group} - -"
|
||||
];
|
||||
};
|
||||
|
||||
users.users."${cfg.user}" = {
|
||||
isSystemUser = true;
|
||||
group = config.services.nginx.group;
|
||||
};
|
||||
};
|
||||
|
||||
meta.maintainers = with maintainers; [ melling ];
|
||||
}
|
|
@ -131,6 +131,7 @@ in {
|
|||
clickhouse = handleTest ./clickhouse.nix {};
|
||||
cloud-init = handleTest ./cloud-init.nix {};
|
||||
cloud-init-hostname = handleTest ./cloud-init-hostname.nix {};
|
||||
cloudlog = handleTest ./cloudlog.nix {};
|
||||
cntr = handleTestOn ["aarch64-linux" "x86_64-linux"] ./cntr.nix {};
|
||||
cockroachdb = handleTestOn ["x86_64-linux"] ./cockroachdb.nix {};
|
||||
collectd = handleTest ./collectd.nix {};
|
||||
|
|
18
nixos/tests/cloudlog.nix
Normal file
18
nixos/tests/cloudlog.nix
Normal file
|
@ -0,0 +1,18 @@
|
|||
import ./make-test-python.nix ({ pkgs, ... }: {
|
||||
name = "cloudlog";
|
||||
meta = {
|
||||
maintainers = with pkgs.lib.maintainers; [ melling ];
|
||||
};
|
||||
nodes = {
|
||||
machine = {
|
||||
services.mysql.package = pkgs.mariadb;
|
||||
services.cloudlog.enable = true;
|
||||
};
|
||||
};
|
||||
testScript = ''
|
||||
start_all()
|
||||
machine.wait_for_unit("phpfpm-cloudlog")
|
||||
machine.wait_for_open_port(80);
|
||||
machine.wait_until_succeeds("curl -s -L --fail http://localhost | grep 'Login - Cloudlog'")
|
||||
'';
|
||||
})
|
|
@ -10,16 +10,16 @@ let
|
|||
inherit tiling_wm;
|
||||
};
|
||||
stableVersion = {
|
||||
version = "2021.3.1.17"; # "Android Studio Dolphin (2021.3.1)"
|
||||
sha256Hash = "sha256-ia2wzg/6RreJTnv+2xQrH11SxDwXHmpsualaSfd3Vso=";
|
||||
version = "2022.1.1.19"; # "Android Studio Electric Eel (2022.1.1)"
|
||||
sha256Hash = "luxE6a2C86JB28ezuIZV49TyE314S1RcNXQnCQamjUA=";
|
||||
};
|
||||
betaVersion = {
|
||||
version = "2022.1.1.12"; # "Android Studio Electric Eel (2022.1.1) Beta 2"
|
||||
sha256Hash = "8iSFPH0PTQkzV1t8bEq7CBtOU8pzdnD/PrpVcgPnO6Q=";
|
||||
version = "2022.2.1.12"; # "Android Studio Flamingo (2022.2.1) Beta 1"
|
||||
sha256Hash = "tIgmX9KiRInIupgIXWgg4dMf8bTwkVopOxAO5O1PUAc=";
|
||||
};
|
||||
latestVersion = { # canary & dev
|
||||
version = "2022.2.1.2"; # "Android Studio Flamingo (2022.2.1) Canary 2"
|
||||
sha256Hash = "hlHlgyl9If2LH4aExpElx0rqmWeoFX+qx4w6RRb5e8U=";
|
||||
version = "2022.3.1.1"; # "Android Studio Girrafe (2022.3.1) Canary 1"
|
||||
sha256Hash = "I7Zc4DDByUB6XOnk7v+91ccpNI7eX/T4d3vH60ih8ec=";
|
||||
};
|
||||
in {
|
||||
# Attributes are named by their corresponding release channels
|
||||
|
|
|
@ -756,8 +756,13 @@ let
|
|||
version = "2.2.6";
|
||||
sha256 = "sha256-1yZeyLrXuubhKzobWcd00F/CdU824uJDTkB6qlHkJlQ=";
|
||||
};
|
||||
meta = {
|
||||
license = lib.licenses.mit;
|
||||
meta = with lib; {
|
||||
changelog = "https://marketplace.visualstudio.com/items/dbaeumer.vscode-eslint/changelog";
|
||||
description = "Integrates ESLint JavaScript into VS Code.";
|
||||
downloadPage = "https://marketplace.visualstudio.com/items?itemName=dbaeumer.vscode-eslint";
|
||||
homepage = "https://github.com/Microsoft/vscode-eslint";
|
||||
license = licenses.mit;
|
||||
maintainers = with maintainers; [ datafoo ];
|
||||
};
|
||||
};
|
||||
|
||||
|
|
63
pkgs/applications/emulators/zsnes/2.x.nix
Normal file
63
pkgs/applications/emulators/zsnes/2.x.nix
Normal file
|
@ -0,0 +1,63 @@
|
|||
{ lib
|
||||
, stdenv
|
||||
, fetchFromGitHub
|
||||
, SDL
|
||||
, libGL
|
||||
, libGLU
|
||||
, libpng
|
||||
, nasm
|
||||
, pkg-config
|
||||
, zlib
|
||||
}:
|
||||
|
||||
stdenv.mkDerivation (finalAttrs: {
|
||||
pname = "zsnes2";
|
||||
version = "2.0.10";
|
||||
|
||||
src = fetchFromGitHub {
|
||||
owner = "xyproto";
|
||||
repo = "zsnes";
|
||||
rev = finalAttrs.version;
|
||||
hash = "sha256-QFPl3I2nFWMmgQRGxrlt4Vh5N4SygvBLjeFiQpgRr8o=";
|
||||
};
|
||||
|
||||
nativeBuildInputs = [
|
||||
nasm
|
||||
pkg-config
|
||||
];
|
||||
|
||||
buildInputs = [
|
||||
SDL
|
||||
libGL
|
||||
libGLU
|
||||
libpng
|
||||
zlib
|
||||
];
|
||||
|
||||
dontConfigure = true;
|
||||
|
||||
NIX_CFLAGS_COMPILE = [
|
||||
# Until upstream fixes the issues...
|
||||
"-Wp,-D_FORTIFY_SOURCE=0"
|
||||
];
|
||||
|
||||
installFlags = [
|
||||
"PREFIX=${placeholder "out"}"
|
||||
];
|
||||
|
||||
postInstall = ''
|
||||
install -Dm644 linux/zsnes.desktop $out/share/applications/zsnes.desktop
|
||||
install -Dm644 icons/16x16x32.png $out/share/icons/hicolor/16x16/apps/zsnes.png
|
||||
install -Dm644 icons/32x32x32.png $out/share/icons/hicolor/32x32/apps/zsnes.png
|
||||
install -Dm644 icons/48x48x32.png $out/share/icons/hicolor/48x48/apps/zsnes.png
|
||||
install -Dm644 icons/64x64x32.png $out/share/icons/hicolor/64x64/apps/zsnes.png
|
||||
'';
|
||||
|
||||
meta = {
|
||||
homepage = "https://github.com/xyproto/zsnes";
|
||||
description = "A maintained fork of zsnes";
|
||||
license = lib.licenses.gpl2Plus;
|
||||
maintainers = [ lib.maintainers.AndersonTorres ];
|
||||
platforms = lib.intersectLists lib.platforms.linux lib.platforms.x86;
|
||||
};
|
||||
})
|
|
@ -13,13 +13,13 @@
|
|||
|
||||
stdenv.mkDerivation (finalAttrs: {
|
||||
pname = "doublecmd";
|
||||
version = "1.0.9";
|
||||
version = "1.0.10";
|
||||
|
||||
src = fetchFromGitHub {
|
||||
owner = "doublecmd";
|
||||
repo = "doublecmd";
|
||||
rev = "v${finalAttrs.version}";
|
||||
hash = "sha256-ruZNHvHBRXRM4h0R571jvasW8rYawq4cn7Hnd9riMnk=";
|
||||
hash = "sha256-S30/exZsw9Rs/l5Sml/q7dqUIcS55ZxbLFYv+M9Jr6o=";
|
||||
};
|
||||
|
||||
nativeBuildInputs = [
|
||||
|
|
|
@ -2,13 +2,13 @@
|
|||
|
||||
stdenv.mkDerivation rec {
|
||||
pname = "kanboard";
|
||||
version = "1.2.25";
|
||||
version = "1.2.26";
|
||||
|
||||
src = fetchFromGitHub {
|
||||
owner = "kanboard";
|
||||
repo = "kanboard";
|
||||
rev = "v${version}";
|
||||
sha256 = "sha256-yBUvePVbNDLYL1d6cNrLBn6+/p1agVzSx29JB3EZ5Fk=";
|
||||
sha256 = "sha256-/Unxl9Vh9pEWjO89sSviGGPFzUwxdb1mbOfpTFTyRL0=";
|
||||
};
|
||||
|
||||
dontBuild = true;
|
||||
|
|
25
pkgs/applications/misc/pomodoro/default.nix
Normal file
25
pkgs/applications/misc/pomodoro/default.nix
Normal file
|
@ -0,0 +1,25 @@
|
|||
{ lib, stdenv, fetchFromGitHub, rustPlatform, Foundation }:
|
||||
|
||||
rustPlatform.buildRustPackage rec {
|
||||
pname = "pomodoro";
|
||||
version = "unstable-2021-06-18";
|
||||
|
||||
src = fetchFromGitHub {
|
||||
owner = "SanderJSA";
|
||||
repo = "Pomodoro";
|
||||
rev = "c833b9551ed0b09e311cdb369cc8226c5b9cac6a";
|
||||
sha256 = "sha256-ZA1q1YVJcdSUF9NTikyT3vrRnqbsu5plzRI2gMu+qnQ=";
|
||||
};
|
||||
|
||||
cargoSha256 = "sha256-6ZhWStZebXSwrej36DXifrsrmR1SWW3PwGUX0hqPwE4=";
|
||||
buildInputs = lib.optionals stdenv.isDarwin [ Foundation ];
|
||||
|
||||
meta = with lib; {
|
||||
description = "A simple CLI pomodoro timer using desktop notifications written in Rust";
|
||||
homepage = "https://github.com/SanderJSA/Pomodoro";
|
||||
license = licenses.mit;
|
||||
maintainers = with maintainers; [ annaaurora ];
|
||||
# error: redefinition of module 'ObjectiveC'
|
||||
broken = stdenv.isDarwin;
|
||||
};
|
||||
}
|
|
@ -442,22 +442,22 @@
|
|||
"vendorHash": "sha256-aVbJT31IIgW0GYzwVX7kT4j7E+dadSbnttThh2lzGyE="
|
||||
},
|
||||
"google": {
|
||||
"hash": "sha256-/UgxXHucsrt960zLQiPruqJLxjFriTrNKjeI1gNEWys=",
|
||||
"hash": "sha256-R104jYttXER/Pzd3ePHh9ZOvpcziuVQK0JcFqdbWtG0=",
|
||||
"homepage": "https://registry.terraform.io/providers/hashicorp/google",
|
||||
"owner": "hashicorp",
|
||||
"proxyVendor": true,
|
||||
"repo": "terraform-provider-google",
|
||||
"rev": "v4.49.0",
|
||||
"rev": "v4.50.0",
|
||||
"spdx": "MPL-2.0",
|
||||
"vendorHash": "sha256-oModEw/gaQCDHLf+2EKf1O1HQSGWnqEReXowE6F7W0o="
|
||||
},
|
||||
"google-beta": {
|
||||
"hash": "sha256-EGwErLYIL0OEIZJQgQizJqqAsZwn1ewPOqAEyg4tC7Q=",
|
||||
"hash": "sha256-OrotSvDNK7PC6nyHEAvmTOYgdYFiHEE8YwfWcOAbPsk=",
|
||||
"homepage": "https://registry.terraform.io/providers/hashicorp/google-beta",
|
||||
"owner": "hashicorp",
|
||||
"proxyVendor": true,
|
||||
"repo": "terraform-provider-google-beta",
|
||||
"rev": "v4.49.0",
|
||||
"rev": "v4.50.0",
|
||||
"spdx": "MPL-2.0",
|
||||
"vendorHash": "sha256-oModEw/gaQCDHLf+2EKf1O1HQSGWnqEReXowE6F7W0o="
|
||||
},
|
||||
|
@ -643,11 +643,11 @@
|
|||
"vendorHash": "sha256-lXQHo66b9X0jZhoF+5Ix5qewQGyI82VPJ7gGzc2CHao="
|
||||
},
|
||||
"kubernetes": {
|
||||
"hash": "sha256-aKGcKmnlYxNS7SrFW2SouRQUXYy339qHrDtQMXGD4DE=",
|
||||
"hash": "sha256-mjxFKCUmXg9CPz/ZZWPr1F8DSUadNroEEwvJgwHYk5s=",
|
||||
"homepage": "https://registry.terraform.io/providers/hashicorp/kubernetes",
|
||||
"owner": "hashicorp",
|
||||
"repo": "terraform-provider-kubernetes",
|
||||
"rev": "v2.16.1",
|
||||
"rev": "v2.17.0",
|
||||
"spdx": "MPL-2.0",
|
||||
"vendorHash": null
|
||||
},
|
||||
|
@ -816,11 +816,11 @@
|
|||
"vendorHash": "sha256-LRIfxQGwG988HE5fftGl6JmBG7tTknvmgpm4Fu1NbWI="
|
||||
},
|
||||
"oci": {
|
||||
"hash": "sha256-nky2PxHA9TznFh6IGrx3UvOuwrGPnQID04qlDQ4/rm4=",
|
||||
"hash": "sha256-EewM1/7zzmJ5KL+/KqstFg6rQT8YpvMULScYeD2ClUQ=",
|
||||
"homepage": "https://registry.terraform.io/providers/oracle/oci",
|
||||
"owner": "oracle",
|
||||
"repo": "terraform-provider-oci",
|
||||
"rev": "v4.104.0",
|
||||
"rev": "v4.104.2",
|
||||
"spdx": "MPL-2.0",
|
||||
"vendorHash": null
|
||||
},
|
||||
|
|
|
@ -19,11 +19,11 @@
|
|||
|
||||
stdenv.mkDerivation rec {
|
||||
pname = "filezilla";
|
||||
version = "3.61.0";
|
||||
version = "3.62.2";
|
||||
|
||||
src = fetchurl {
|
||||
url = "https://download.filezilla-project.org/client/FileZilla_${version}_src.tar.bz2";
|
||||
hash = "sha256-Cv7w5NolICaHsy7Wsf/NhELVs1vc0W308Cuy6pLimfc=";
|
||||
hash = "sha256-p2cJY1yg6kdPaR9sYLGRM0rzB57xksB8NGUEuqtzjBI=";
|
||||
};
|
||||
|
||||
configureFlags = [
|
||||
|
|
43
pkgs/applications/radio/cloudlog/default.nix
Normal file
43
pkgs/applications/radio/cloudlog/default.nix
Normal file
|
@ -0,0 +1,43 @@
|
|||
{ lib
|
||||
, stdenvNoCC
|
||||
, fetchFromGitHub
|
||||
, nixosTests
|
||||
, php}:
|
||||
|
||||
stdenvNoCC.mkDerivation rec {
|
||||
name = "cloudlog";
|
||||
version = "2.3";
|
||||
|
||||
src = fetchFromGitHub {
|
||||
owner = "magicbug";
|
||||
repo = "Cloudlog";
|
||||
rev = version;
|
||||
sha256 = "sha256-IepCeV/mYy/GEzRTXf67LYQQaN5Rj5Z77KaF2l30r60=";
|
||||
};
|
||||
|
||||
postPath = ''
|
||||
substituteInPlace index.php \
|
||||
--replace "define('ENVIRONMENT', 'development');" "define('ENVIRONMENT', 'production');"
|
||||
'';
|
||||
|
||||
installPhase = ''
|
||||
mkdir $out/
|
||||
cp -R ./* $out
|
||||
'';
|
||||
|
||||
passthru.tests = {
|
||||
inherit (nixosTests) cloudlog;
|
||||
};
|
||||
|
||||
meta = with lib; {
|
||||
description = ''
|
||||
Web based amateur radio logging application built using PHP & MySQL
|
||||
supports general station logging tasks from HF to Microwave with
|
||||
supporting applications to support CAT control.
|
||||
'';
|
||||
license = licenses.mit;
|
||||
homepage = "https://www.magicbug.co.uk/cloudlog";
|
||||
platforms = php.meta.platforms;
|
||||
maintainers = with maintainers; [ melling ];
|
||||
};
|
||||
}
|
|
@ -6,13 +6,13 @@
|
|||
|
||||
stdenv.mkDerivation rec {
|
||||
pname = "gridtracker";
|
||||
version = "1.22.1226";
|
||||
version = "1.23.0110";
|
||||
|
||||
src = fetchFromGitLab {
|
||||
owner = "gridtracker.org";
|
||||
repo = "gridtracker";
|
||||
rev = "v${version}";
|
||||
sha256 = "sha256-/Noc2aqHBjphX6RDqxQBI/OOKZgEnOndn0daBt1edXM=";
|
||||
sha256 = "sha256-yQWdBNt7maYTzroB+P1hsGIeivkP+soR3/b847HLYZY=";
|
||||
};
|
||||
|
||||
postPatch = ''
|
||||
|
|
|
@ -42,13 +42,13 @@
|
|||
|
||||
mkDerivation rec {
|
||||
pname = "sdrangel";
|
||||
version = "7.8.5";
|
||||
version = "7.8.6";
|
||||
|
||||
src = fetchFromGitHub {
|
||||
owner = "f4exb";
|
||||
repo = "sdrangel";
|
||||
rev = "v${version}";
|
||||
sha256 = "sha256-m5b51rR2l4EdF2kMogHIi1ojoy3UwuU0Q3pfB1ev300=";
|
||||
sha256 = "sha256-tLU2OHFf1PPNRr1t3MWWCKnvILp1DW0k4TAxrXWI2X4=";
|
||||
};
|
||||
|
||||
nativeBuildInputs = [ cmake pkg-config ];
|
||||
|
|
|
@ -8,9 +8,11 @@
|
|||
, pkg-config
|
||||
, pantheon
|
||||
, python3
|
||||
, curl
|
||||
, gettext
|
||||
, glib
|
||||
, gtk3
|
||||
, json-glib
|
||||
, libwnck
|
||||
, libgee
|
||||
, libgtop
|
||||
|
@ -25,13 +27,13 @@
|
|||
|
||||
stdenv.mkDerivation rec {
|
||||
pname = "monitor";
|
||||
version = "0.14.0";
|
||||
version = "0.15.0";
|
||||
|
||||
src = fetchFromGitHub {
|
||||
owner = "stsdc";
|
||||
repo = "monitor";
|
||||
rev = version;
|
||||
sha256 = "sha256-dw1FR9nU8MY6LBL3sF942azeSgKmCntXCk4+nhMb4Wo=";
|
||||
sha256 = "sha256-w4c9rVO54mrjUX2iRxUQ7PHqE+8D+BqBgHMK2X9nI0g=";
|
||||
fetchSubmodules = true;
|
||||
};
|
||||
|
||||
|
@ -46,8 +48,10 @@ stdenv.mkDerivation rec {
|
|||
];
|
||||
|
||||
buildInputs = [
|
||||
curl
|
||||
glib
|
||||
gtk3
|
||||
json-glib
|
||||
pantheon.granite
|
||||
pantheon.wingpanel
|
||||
libgee
|
||||
|
@ -72,6 +76,11 @@ stdenv.mkDerivation rec {
|
|||
postPatch = ''
|
||||
chmod +x meson/post_install.py
|
||||
patchShebangs meson/post_install.py
|
||||
|
||||
# Alternatively, using pkg-config here should just work.
|
||||
substituteInPlace meson.build --replace \
|
||||
"meson.get_compiler('c').find_library('libcurl', dirs: vapidir)" \
|
||||
"meson.get_compiler('c').find_library('libcurl', dirs: '${curl.out}/lib')"
|
||||
'';
|
||||
|
||||
passthru = {
|
||||
|
|
|
@ -7,16 +7,16 @@
|
|||
|
||||
rustPlatform.buildRustPackage rec {
|
||||
pname = "git-cliff";
|
||||
version = "1.1.1";
|
||||
version = "1.1.2";
|
||||
|
||||
src = fetchFromGitHub {
|
||||
owner = "orhun";
|
||||
repo = "git-cliff";
|
||||
rev = "v${version}";
|
||||
hash = "sha256-GCHwpOfjti9PETy3cHFHBFBot6YcSSFTBCd3zEtpP3U=";
|
||||
hash = "sha256-QYldwxQYod5qkNC3soiKoCLDFR4UaLxdGkVufn1JIeE=";
|
||||
};
|
||||
|
||||
cargoHash = "sha256-76HWkfct9weA64yvY5G/l96mjNpuKjPYHFZ5Ctz43Us=";
|
||||
cargoHash = "sha256-jwDJb9Hl0PegCufmaj1Q3h5itgt26E4dwmcyCxZ+4FM=";
|
||||
|
||||
# attempts to run the program on .git in src which is not deterministic
|
||||
doCheck = false;
|
||||
|
|
|
@ -1,7 +1,8 @@
|
|||
{ lib, mkDerivation, fetchFromGitHub, fetchpatch, which, qtbase, qtwebkit, qtscript
|
||||
, libpulseaudio, fftwSinglePrec , lame, zlib, libGLU, libGL, alsa-lib, freetype
|
||||
, perl, pkg-config , libsamplerate, libbluray, lzo, libX11, libXv, libXrandr, libXvMC, libXinerama, libXxf86vm
|
||||
, libXmu , yasm, libuuid, taglib, libtool, autoconf, automake, file, exiv2, linuxHeaders, soundtouch, libzip
|
||||
, libXmu , yasm, libuuid, taglib, libtool, autoconf, automake, file, exiv2, linuxHeaders
|
||||
, soundtouch, libzip, libhdhomerun
|
||||
, withWebKit ? false
|
||||
}:
|
||||
|
||||
|
@ -35,6 +36,7 @@ mkDerivation rec {
|
|||
freetype qtbase qtscript lame zlib libGLU libGL
|
||||
perl libsamplerate libbluray lzo alsa-lib libpulseaudio fftwSinglePrec libX11 libXv libXrandr libXvMC
|
||||
libXmu libXinerama libXxf86vm libXmu libuuid taglib exiv2 soundtouch libzip
|
||||
libhdhomerun
|
||||
] ++ lib.optional withWebKit qtwebkit;
|
||||
nativeBuildInputs = [ pkg-config which yasm libtool autoconf automake file ];
|
||||
|
||||
|
|
|
@ -7,13 +7,13 @@
|
|||
|
||||
stdenv.mkDerivation rec {
|
||||
pname = "obs-move-transition";
|
||||
version = "2.7.1";
|
||||
version = "2.8.0";
|
||||
|
||||
src = fetchFromGitHub {
|
||||
owner = "exeldro";
|
||||
repo = "obs-move-transition";
|
||||
rev = version;
|
||||
sha256 = "sha256-zWHQ01iNTlqSAKcmsDCUZPXmmBIpqY/ZDftD5J6kp80=";
|
||||
sha256 = "sha256-v4mAv4dqurM2S4/vM1APge0xoMLnOaigGU15vjNxxSo=";
|
||||
};
|
||||
|
||||
nativeBuildInputs = [ cmake ];
|
||||
|
|
|
@ -1,16 +1,11 @@
|
|||
{ stdenv
|
||||
, bazel
|
||||
, cacert
|
||||
, lib
|
||||
}:
|
||||
|
||||
let
|
||||
bazelPkg = bazel;
|
||||
in
|
||||
|
||||
args@{
|
||||
name ? "${args.pname}-${args.version}"
|
||||
, bazel ? bazelPkg
|
||||
, bazel
|
||||
, bazelFlags ? []
|
||||
, bazelBuildFlags ? []
|
||||
, bazelTestFlags ? []
|
||||
|
|
|
@ -1,5 +1,5 @@
|
|||
{
|
||||
"version": "0.12.0",
|
||||
"sha256": "sha256-ZieKL98EUT3RbZ1UZkhrnXjg3N0RATKB69F8D7IWnJ8=",
|
||||
"depsSha256": "sha256-Otm8koWrDYxodfliIe+q4U+39eStR5umEKnQQmOOGeA="
|
||||
"version": "0.13.0",
|
||||
"sha256": "sha256-eUAlnEKhoJ3j2Ii2EBL620jv3aGeMJcWoMMG+vWIdm4=",
|
||||
"depsSha256": "sha256-fAt9BpEE9truGWpor0BttVd9aNZlgQ6UTorIEcJ82wM="
|
||||
}
|
||||
|
|
|
@ -28,7 +28,6 @@ let
|
|||
|
||||
## Files in versions/ are generated automatically by update.sh ##
|
||||
dotnet_3_1 = import ./versions/3.1.nix (buildAttrs // { icu = icu70; });
|
||||
dotnet_5_0 = import ./versions/5.0.nix (buildAttrs // { inherit icu; });
|
||||
dotnet_6_0 = import ./versions/6.0.nix (buildAttrs // { inherit icu; });
|
||||
dotnet_7_0 = import ./versions/7.0.nix (buildAttrs // { inherit icu; });
|
||||
in
|
||||
|
@ -38,7 +37,8 @@ rec {
|
|||
combinePackages = attrs: callPackage (import ./combine-packages.nix attrs) {};
|
||||
|
||||
# EOL
|
||||
sdk_2_1 = throw "Dotnet SDK 2.1 is EOL, please use 3.1 (LTS), 5.0 (Current) or 6.0 (LTS)";
|
||||
sdk_2_2 = throw "Dotnet SDK 2.2 is EOL, please use 3.1 (LTS), 5.0 (Current) or 6.0 (LTS)";
|
||||
sdk_3_0 = throw "Dotnet SDK 3.0 is EOL, please use 3.1 (LTS), 5.0 (Current) or 6.0 (LTS)";
|
||||
} // dotnet_3_1 // dotnet_5_0 // dotnet_6_0 // dotnet_7_0
|
||||
sdk_2_1 = throw "Dotnet SDK 2.1 is EOL, please use 6.0 (LTS) or 7.0 (Current)";
|
||||
sdk_2_2 = throw "Dotnet SDK 2.2 is EOL, please use 6.0 (LTS) or 7.0 (Current)";
|
||||
sdk_3_0 = throw "Dotnet SDK 3.0 is EOL, please use 6.0 (LTS) or 7.0 (Current)";
|
||||
sdk_5_0 = throw "Dotnet SDK 5.0 is EOL, please use 6.0 (LTS) or 7.0 (Current)";
|
||||
} // dotnet_3_1 // dotnet_6_0 // dotnet_7_0
|
||||
|
|
|
@ -1,137 +0,0 @@
|
|||
{ buildAspNetCore, buildNetRuntime, buildNetSdk, icu }:
|
||||
|
||||
# v5.0 (eol)
|
||||
{
|
||||
aspnetcore_5_0 = buildAspNetCore {
|
||||
inherit icu;
|
||||
version = "5.0.17";
|
||||
srcs = {
|
||||
x86_64-linux = {
|
||||
url = "https://download.visualstudio.microsoft.com/download/pr/a2b96f83-e22a-4fa6-a10e-709b3effac9a/0d6ade6c0ceebc8ef7dbf2b1a6d86f17/aspnetcore-runtime-5.0.17-linux-x64.tar.gz";
|
||||
sha512 = "d8e87804e9e86273c6512785bd5a6f0e834ff3f4bbebc11c4fcdf16ab4fdfabd0d981a756955267c1aa9bbeec596de3728ce9b2e6415d2d80daef0d999a5df6d";
|
||||
};
|
||||
aarch64-linux = {
|
||||
url = "https://download.visualstudio.microsoft.com/download/pr/6eb8aee2-cbea-4c4f-9bb9-ea6229ec229b/d6c438e5071c359ad995134f0a33e731/aspnetcore-runtime-5.0.17-linux-arm64.tar.gz";
|
||||
sha512 = "ac1a9d89f1b730dfdca9c2e48373ef21f8f9316014eefbe6b11516f8195d3b3efc4e482883774b74ea2ff1cb77174a2cb471bd1157ab5b7d71621e3026c38e9b";
|
||||
};
|
||||
x86_64-darwin = {
|
||||
url = "https://download.visualstudio.microsoft.com/download/pr/25e4817f-6fd0-46dc-be0d-d819445bac5c/a8fa228c872df683741c8a79745f8fb3/aspnetcore-runtime-5.0.17-osx-x64.tar.gz";
|
||||
sha512 = "bb0c43c723090fa2d8a0255e6fc8c004ebe7baf2d5d56e22ad2e6336a67fe415333d451e459c8857c0ccb5819d998232c9617bf45f222559d4b8891b0af41f20";
|
||||
};
|
||||
};
|
||||
};
|
||||
|
||||
runtime_5_0 = buildNetRuntime {
|
||||
inherit icu;
|
||||
version = "5.0.17";
|
||||
srcs = {
|
||||
x86_64-linux = {
|
||||
url = "https://download.visualstudio.microsoft.com/download/pr/e77438f6-865f-45e0-9a52-3e4b04aa609f/024a880ed4bfbfd3b9f222fec0b6aaff/dotnet-runtime-5.0.17-linux-x64.tar.gz";
|
||||
sha512 = "a9c4784930a977abbc42aff1337dda06ec588c1ec4769a59f9fcab4d5df4fc9efe65f8e61e5433db078f67a94ea2dfe870c32c482a50d4c16283ffacacff4261";
|
||||
};
|
||||
aarch64-linux = {
|
||||
url = "https://download.visualstudio.microsoft.com/download/pr/6690730f-cf10-40f1-9d4d-4c0d002f22d0/e117133858f190c169873200b8d7b9d7/dotnet-runtime-5.0.17-linux-arm64.tar.gz";
|
||||
sha512 = "99cb11871924d3abedcc9c8079c54bc0c550203c7cbe4e349ed70d4355f40e4620b68d90b797e6461d898c06bed6953580e2cd4ad01483e5de107ca5a3409610";
|
||||
};
|
||||
x86_64-darwin = {
|
||||
url = "https://download.visualstudio.microsoft.com/download/pr/39326cf0-dc7f-42a3-9f7a-fe30c75c7a7f/33cbce552148e13d47120fe4502f5b5e/dotnet-runtime-5.0.17-osx-x64.tar.gz";
|
||||
sha512 = "31add512418640f98bc9511509db2049a2674c7725169d26be89218a02ac7972e03e5d6be5a3d45a0dfa764e6eade503a8f4957b7b198ec6ad412e423d95f1b9";
|
||||
};
|
||||
};
|
||||
};
|
||||
|
||||
sdk_5_0 = buildNetSdk {
|
||||
inherit icu;
|
||||
version = "5.0.408";
|
||||
srcs = {
|
||||
x86_64-linux = {
|
||||
url = "https://download.visualstudio.microsoft.com/download/pr/904da7d0-ff02-49db-bd6b-5ea615cbdfc5/966690e36643662dcc65e3ca2423041e/dotnet-sdk-5.0.408-linux-x64.tar.gz";
|
||||
sha512 = "abbf22c420df2d8398d1616efa3d31e1b8f96130697746c45ad68668676d12e65ec3b4dd75f28a5dc7607da58b6e369693c0e658def15ce2431303c28e99db55";
|
||||
};
|
||||
aarch64-linux = {
|
||||
url = "https://download.visualstudio.microsoft.com/download/pr/d4b71fac-a2fd-4516-ac58-100fb09d796a/e79d6c2a8040b59bf49c0d167ae70a7b/dotnet-sdk-5.0.408-linux-arm64.tar.gz";
|
||||
sha512 = "50f23d7aca91051d8b7c37f1a76b1eb51e6fe73e017d98558d757a6b9699e4237d401ce81515c1601b8c21eb62fee4e0b4f0bbed8967eefa3ceba75fc242f01b";
|
||||
};
|
||||
x86_64-darwin = {
|
||||
url = "https://download.visualstudio.microsoft.com/download/pr/4aeecc7c-7ffa-418f-9362-cf5eb3ed0396/055d5e6064a9fdecd7d906f5f262373d/dotnet-sdk-5.0.408-osx-x64.tar.gz";
|
||||
sha512 = "3fdd4deac2809b00c0f669d5488000ac1b9a47dee6ab7b31167d7cec4759a10ee347fd4f52090a40684e5ecc1e1f57eb99c558e561edfd1436a2f77fc1c1a0b2";
|
||||
};
|
||||
};
|
||||
packages = { fetchNuGet }: [
|
||||
(fetchNuGet { pname = "Microsoft.AspNetCore.App.Runtime.linux-arm"; version = "5.0.17"; sha256 = "0mfawgcc23r44a1r7ynafxwga6jzn0f0z5ys03qssrvlcdsb376x"; })
|
||||
(fetchNuGet { pname = "Microsoft.AspNetCore.App.Runtime.linux-arm64"; version = "5.0.17"; sha256 = "183xgqzlwd5lhacxdwcjl8vcq7r7xypv0hddps9k32mmmwf83d8h"; })
|
||||
(fetchNuGet { pname = "Microsoft.AspNetCore.App.Runtime.linux-musl-arm64"; version = "5.0.17"; sha256 = "0i5pp1smjkyhiyhcbkyc3cxz0sx9204bfml8wsdy7bxznbh2gkmw"; })
|
||||
(fetchNuGet { pname = "Microsoft.AspNetCore.App.Runtime.linux-musl-x64"; version = "5.0.17"; sha256 = "1fmd9jq2nzy63hjh4sa6zl636wpgwr3r8ahzln5w14m9k87lfdbk"; })
|
||||
(fetchNuGet { pname = "Microsoft.AspNetCore.App.Runtime.linux-x64"; version = "5.0.17"; sha256 = "066fwdlssbv556zd9w1x87x1j8j4kafj9rxyy0692bssdb4gcyc8"; })
|
||||
(fetchNuGet { pname = "Microsoft.AspNetCore.App.Runtime.osx-x64"; version = "5.0.17"; sha256 = "1qvvqf8mmzzc7a7fhx324dprnbxhknr3qxspb2xhsn3yyg44xn2d"; })
|
||||
(fetchNuGet { pname = "Microsoft.AspNetCore.App.Runtime.win-arm"; version = "5.0.17"; sha256 = "1gzf2gv4z9bn1cr1kpqpf1jf7m0p0wd1pxq5ndylq6bw353yglk1"; })
|
||||
(fetchNuGet { pname = "Microsoft.AspNetCore.App.Runtime.win-arm64"; version = "5.0.17"; sha256 = "1lml70ln9bfjrfjf3jbxfzd5kgd4cp4h7v052md5ja364g7lalsy"; })
|
||||
(fetchNuGet { pname = "Microsoft.AspNetCore.App.Runtime.win-x64"; version = "5.0.17"; sha256 = "0j90fri15c05lw96xybgvqkysfm7g8grhkrg25g75vhi6ni2ricj"; })
|
||||
(fetchNuGet { pname = "Microsoft.AspNetCore.App.Runtime.win-x86"; version = "5.0.17"; sha256 = "1bdb887xvgxsmphys83zp9skn848p1r8viclc8p29w1rby4wi19i"; })
|
||||
(fetchNuGet { pname = "Microsoft.NETCore.App.Host.linux-arm"; version = "5.0.17"; sha256 = "0y90p765sj54clf2bwrka99w73g8b9550b4qvyilqggzydl1c1hk"; })
|
||||
(fetchNuGet { pname = "Microsoft.NETCore.App.Host.linux-arm64"; version = "5.0.17"; sha256 = "07v7vyqm556xr1ypkazfp6gh6drgf20zkwbhkpja8bwdcr6lphbb"; })
|
||||
(fetchNuGet { pname = "Microsoft.NETCore.App.Host.linux-musl-arm64"; version = "5.0.17"; sha256 = "0sbzlzhazh31s63hw9553hk9j56fxssncmfgidiyh0dg73aacrsp"; })
|
||||
(fetchNuGet { pname = "Microsoft.NETCore.App.Host.linux-musl-x64"; version = "5.0.17"; sha256 = "1qxphvlr882rvmj71y2imnf6r3hh4ln2n138qjyv1z129dp2g4y1"; })
|
||||
(fetchNuGet { pname = "Microsoft.NETCore.App.Host.linux-x64"; version = "5.0.17"; sha256 = "1lc2jhr4ikffi5ylyf8f6ya6k0hdj0wp1l0017grrwd4m5ajj4vv"; })
|
||||
(fetchNuGet { pname = "Microsoft.NETCore.App.Host.osx-x64"; version = "5.0.17"; sha256 = "02g5w41ivrw3n6cy3l3ixhcl8bw1fsv4bzs2m34k9h5fqmliaf3c"; })
|
||||
(fetchNuGet { pname = "Microsoft.NETCore.App.Host.win-arm"; version = "5.0.17"; sha256 = "07rfkxpf6rp8x0lybl8hx40mk09w5gjrr9djkjcp8lvjgzidnxq9"; })
|
||||
(fetchNuGet { pname = "Microsoft.NETCore.App.Host.win-arm64"; version = "5.0.17"; sha256 = "1i7wka56n3akr96jrkj37jx98bwxfzhpx5705930v50izligd08x"; })
|
||||
(fetchNuGet { pname = "Microsoft.NETCore.App.Host.win-x64"; version = "5.0.17"; sha256 = "15f1kqlpp1d05dhg3dfya32vvzbpj6c7gxds947f10jb0hqlnhdj"; })
|
||||
(fetchNuGet { pname = "Microsoft.NETCore.App.Host.win-x86"; version = "5.0.17"; sha256 = "1j1334zxv815ksdnllnbwwsbwnimjlpknjmqy1riy2zpswxlfkz6"; })
|
||||
(fetchNuGet { pname = "Microsoft.NETCore.App.Runtime.linux-arm"; version = "5.0.17"; sha256 = "0mmgd6nacx4fzf0w02ch0qxa43vrv6wfspykxsy2bkpvrnvr8xr9"; })
|
||||
(fetchNuGet { pname = "Microsoft.NETCore.App.Runtime.linux-arm64"; version = "5.0.17"; sha256 = "16whaq82pj6fqa0vam3a0va9ly843aa1z12hza040vn6252kk9fq"; })
|
||||
(fetchNuGet { pname = "Microsoft.NETCore.App.Runtime.linux-musl-arm64"; version = "5.0.17"; sha256 = "1zavnwqvn2f7lhb880wgv02anrvqsh6l34w72knwd31irggph08l"; })
|
||||
(fetchNuGet { pname = "Microsoft.NETCore.App.Runtime.linux-musl-x64"; version = "5.0.17"; sha256 = "173r2srcbad2prrw3l914scmdks3mghxgszvlwypdjnv0f2szgvv"; })
|
||||
(fetchNuGet { pname = "Microsoft.NETCore.App.Runtime.linux-x64"; version = "5.0.17"; sha256 = "0jgcfs3jc98jfyaaamssznckbpnaygplk8pjsp6dswpansz5bnnq"; })
|
||||
(fetchNuGet { pname = "Microsoft.NETCore.App.Runtime.osx-x64"; version = "5.0.17"; sha256 = "1ph5kx18syinp8bpzw80bgq3njl65gwzws727xcmxnysgm7snmjp"; })
|
||||
(fetchNuGet { pname = "Microsoft.NETCore.App.Runtime.win-arm"; version = "5.0.17"; sha256 = "0m4jhn70parwnl18fql0sk9sf14y8cf08xw6x2cm5bfhnc9jvjny"; })
|
||||
(fetchNuGet { pname = "Microsoft.NETCore.App.Runtime.win-arm64"; version = "5.0.17"; sha256 = "1af20jkv73767b4fy18s2dvjncaca1ny0csyr7wbhvqfs59y3n1x"; })
|
||||
(fetchNuGet { pname = "Microsoft.NETCore.App.Runtime.win-x64"; version = "5.0.17"; sha256 = "0llhsi03wyp2yjqy0snywqgwjgam91i4nsf5lc9kaxkk5h6vj1a0"; })
|
||||
(fetchNuGet { pname = "Microsoft.NETCore.App.Runtime.win-x86"; version = "5.0.17"; sha256 = "0xvprbjwd3fymddvavsy7wk5q2hp45hdi10qz4rdbmns23vqkzmf"; })
|
||||
(fetchNuGet { pname = "Microsoft.NETCore.DotNetAppHost"; version = "5.0.17"; sha256 = "0vhvxpba3i9ffp4gp56l3rnlhq9yg07n3dv5qi89zb90vgyqjh1p"; })
|
||||
(fetchNuGet { pname = "Microsoft.NETCore.DotNetHost"; version = "5.0.17"; sha256 = "074c9byxwmndfdavxn103220f5gklaaxc9wj7zpb5v3yr3ads30f"; })
|
||||
(fetchNuGet { pname = "Microsoft.NETCore.DotNetHostPolicy"; version = "5.0.17"; sha256 = "03jkkpsy2zjfp722fa2fcnpk2g6jzy0bn9vip5c39k78y5pz29x6"; })
|
||||
(fetchNuGet { pname = "Microsoft.NETCore.DotNetHostResolver"; version = "5.0.17"; sha256 = "1ih6c104skp9q17i2dnsma45l6nv5c62vv2i1988dcjw2v0sl98m"; })
|
||||
(fetchNuGet { pname = "runtime.linux-arm64.Microsoft.NETCore.DotNetAppHost"; version = "5.0.17"; sha256 = "0gwsxd1l0n32xnw0lyjixj2634iyygdb8pd7chydsr3qk8njxnpk"; })
|
||||
(fetchNuGet { pname = "runtime.linux-arm64.Microsoft.NETCore.DotNetHost"; version = "5.0.17"; sha256 = "0x5dhn1jkwqnd0cki1vi97rhyfac6w79hvh9dxvnkn2k04sbps8q"; })
|
||||
(fetchNuGet { pname = "runtime.linux-arm64.Microsoft.NETCore.DotNetHostPolicy"; version = "5.0.17"; sha256 = "1ipx3qn78z6gi415c4fa9wgy8k75aifbml6ys1c9ghl6yxbv0fd0"; })
|
||||
(fetchNuGet { pname = "runtime.linux-arm64.Microsoft.NETCore.DotNetHostResolver"; version = "5.0.17"; sha256 = "1wgbx648yndl0hh8vx6sflfwjyr5pfhi7vj7v19l6vxnrr1096w7"; })
|
||||
(fetchNuGet { pname = "runtime.linux-arm.Microsoft.NETCore.DotNetAppHost"; version = "5.0.17"; sha256 = "17jc8jc2dk1g8996jpq3k0g6c5inijivxkbz0grxrgr5jbyiv19y"; })
|
||||
(fetchNuGet { pname = "runtime.linux-arm.Microsoft.NETCore.DotNetHost"; version = "5.0.17"; sha256 = "0ydn40qn6cs6f20byvmc9j008s6csxjbh6jh5w4q995vipcmcpcj"; })
|
||||
(fetchNuGet { pname = "runtime.linux-arm.Microsoft.NETCore.DotNetHostPolicy"; version = "5.0.17"; sha256 = "0bw08wlf96vcyix850y8jips1glrz2cbj647af4d7gggw8p3wwzw"; })
|
||||
(fetchNuGet { pname = "runtime.linux-arm.Microsoft.NETCore.DotNetHostResolver"; version = "5.0.17"; sha256 = "0xsqyw848scwcz09pgc719776q712xabx4xv47srzij34p2pq7np"; })
|
||||
(fetchNuGet { pname = "runtime.linux-musl-arm64.Microsoft.NETCore.DotNetAppHost"; version = "5.0.17"; sha256 = "00b0vipypjai4l8icr74kjhglxx2xlc3nw3vyiwisg52l9zyby66"; })
|
||||
(fetchNuGet { pname = "runtime.linux-musl-arm64.Microsoft.NETCore.DotNetHost"; version = "5.0.17"; sha256 = "1cdgd4p5zr1mzz9hlb5mj946zfa1vn9wya5y2bhqn9y4ak831wzp"; })
|
||||
(fetchNuGet { pname = "runtime.linux-musl-arm64.Microsoft.NETCore.DotNetHostPolicy"; version = "5.0.17"; sha256 = "17v8m4fxm4q40z49a2h4lw9dawg6pwfv4s2dskzc23ggcjgr6dp1"; })
|
||||
(fetchNuGet { pname = "runtime.linux-musl-arm64.Microsoft.NETCore.DotNetHostResolver"; version = "5.0.17"; sha256 = "1fbqi92prqmvxx0rx7vhl10l665jmmhb2ng5jndimggydb0ckpqh"; })
|
||||
(fetchNuGet { pname = "runtime.linux-musl-x64.Microsoft.NETCore.DotNetAppHost"; version = "5.0.17"; sha256 = "1rijxkzzk65xs9z2ygs13h0rhw1cli5vwshmvs1gfnwhhn8ic0gx"; })
|
||||
(fetchNuGet { pname = "runtime.linux-musl-x64.Microsoft.NETCore.DotNetHost"; version = "5.0.17"; sha256 = "02mxvpm2zs5jvawigvxlnrw6si4zwj6qlcas99m9xdmm8yqq22cm"; })
|
||||
(fetchNuGet { pname = "runtime.linux-musl-x64.Microsoft.NETCore.DotNetHostPolicy"; version = "5.0.17"; sha256 = "0c1lcl3yy88vdfw12c7h0ww596qfjd5f8l2mn7mlqs6i3f864bkg"; })
|
||||
(fetchNuGet { pname = "runtime.linux-musl-x64.Microsoft.NETCore.DotNetHostResolver"; version = "5.0.17"; sha256 = "0w0wg9ah7vngvpyds67l6qhizpkdf2r6m6cqyyvv3s5dw5l8rxin"; })
|
||||
(fetchNuGet { pname = "runtime.linux-x64.Microsoft.NETCore.DotNetAppHost"; version = "5.0.17"; sha256 = "17yy7605vkfz0f4h58005gdfg6fnjxlcnq0vg0hrxsgbdqmd7p1i"; })
|
||||
(fetchNuGet { pname = "runtime.linux-x64.Microsoft.NETCore.DotNetHost"; version = "5.0.17"; sha256 = "0av25fgkdl7zvn44wp8gqx2xl2mdlv1f9cgxzp7xk5yq8f7ynxpq"; })
|
||||
(fetchNuGet { pname = "runtime.linux-x64.Microsoft.NETCore.DotNetHostPolicy"; version = "5.0.17"; sha256 = "1smhmdfq0jlv1gq18hdaj0y9yzkvqzmki19c0b3j5b76yxxxpbwz"; })
|
||||
(fetchNuGet { pname = "runtime.linux-x64.Microsoft.NETCore.DotNetHostResolver"; version = "5.0.17"; sha256 = "0n0cdb9zpdb4h4v6r265pqmqg8c94ydywvna6jp1c6qhqlr0qk39"; })
|
||||
(fetchNuGet { pname = "runtime.osx-x64.Microsoft.NETCore.DotNetAppHost"; version = "5.0.17"; sha256 = "1s2n2sx29c8rx549zizj8yrddjl98a7vwvxw56y0jvvbwphr9gz4"; })
|
||||
(fetchNuGet { pname = "runtime.osx-x64.Microsoft.NETCore.DotNetHost"; version = "5.0.17"; sha256 = "19m66yvv0hnmyrmx2l4drbls0fcib75fxq2csdx6p8gd54bnrsh3"; })
|
||||
(fetchNuGet { pname = "runtime.osx-x64.Microsoft.NETCore.DotNetHostPolicy"; version = "5.0.17"; sha256 = "0bcnlsxcrvhybcjbb9879njx0c4z76y7djx4643g1rpjnkcrj9ww"; })
|
||||
(fetchNuGet { pname = "runtime.osx-x64.Microsoft.NETCore.DotNetHostResolver"; version = "5.0.17"; sha256 = "1bf95h2f0dmpmv7z7961zia5vaqvmjq3wkf6iil9jxv4z674624w"; })
|
||||
(fetchNuGet { pname = "runtime.win-arm64.Microsoft.NETCore.DotNetAppHost"; version = "5.0.17"; sha256 = "02q593q09mwwh23m86048vc7b7an7pqch5nd86d4hxzkamnpnpsa"; })
|
||||
(fetchNuGet { pname = "runtime.win-arm64.Microsoft.NETCore.DotNetHost"; version = "5.0.17"; sha256 = "16vzxywfj88gjcwfnmcb6b50ld8dp46i4pqiwwcy7yz15xgdhbm2"; })
|
||||
(fetchNuGet { pname = "runtime.win-arm64.Microsoft.NETCore.DotNetHostPolicy"; version = "5.0.17"; sha256 = "1ix5lg2j5ihdfp9j3jdxc042g4syjzc4bafid465j52h6znsm6wm"; })
|
||||
(fetchNuGet { pname = "runtime.win-arm64.Microsoft.NETCore.DotNetHostResolver"; version = "5.0.17"; sha256 = "0w30v8r26cg427n5glm9nz6r10baalkqq5icqqxkq71hmh8fsjqb"; })
|
||||
(fetchNuGet { pname = "runtime.win-arm.Microsoft.NETCore.DotNetAppHost"; version = "5.0.17"; sha256 = "168iq4hdp6bhdpgqa1mir1bygmh2ggwkys1r82d6kpl2lzbxjy28"; })
|
||||
(fetchNuGet { pname = "runtime.win-arm.Microsoft.NETCore.DotNetHost"; version = "5.0.17"; sha256 = "18jpw2wbrb1b941729lb7hiq4yfq2z53pcxwz4mpgawnr58y0562"; })
|
||||
(fetchNuGet { pname = "runtime.win-arm.Microsoft.NETCore.DotNetHostPolicy"; version = "5.0.17"; sha256 = "0ig464fcsj2jr0p02f6slifwf1m0408g95npm0vccf5ww1nbgkpi"; })
|
||||
(fetchNuGet { pname = "runtime.win-arm.Microsoft.NETCore.DotNetHostResolver"; version = "5.0.17"; sha256 = "0qj5avmjrvabxzimprg4m54k3p6zkwrhbpv0byc8c9gbi47s323j"; })
|
||||
(fetchNuGet { pname = "runtime.win-x64.Microsoft.NETCore.DotNetAppHost"; version = "5.0.17"; sha256 = "05ghz164lpff7n8mrxs7jm2h8n3clsg4w953zrag3k5ry9j36m9c"; })
|
||||
(fetchNuGet { pname = "runtime.win-x64.Microsoft.NETCore.DotNetHost"; version = "5.0.17"; sha256 = "0azgs542mbg69jlc81529i2z5m728w8sc2i9m5dx15hvxqqqcjiz"; })
|
||||
(fetchNuGet { pname = "runtime.win-x64.Microsoft.NETCore.DotNetHostPolicy"; version = "5.0.17"; sha256 = "12n1kcgcv5z8hkvjqfk0n705kcipbai4sgcwiimi52xpaf34xw8m"; })
|
||||
(fetchNuGet { pname = "runtime.win-x64.Microsoft.NETCore.DotNetHostResolver"; version = "5.0.17"; sha256 = "0b1s2m0a7xcdzfz22x6k7v5hkca90azdjk6pw7wwdnvszwq26nxp"; })
|
||||
(fetchNuGet { pname = "runtime.win-x86.Microsoft.NETCore.DotNetAppHost"; version = "5.0.17"; sha256 = "1sjpq07swgj0isdgyh6p2yb254qb9781lv44xfhj6nz7mx2yhdh1"; })
|
||||
(fetchNuGet { pname = "runtime.win-x86.Microsoft.NETCore.DotNetHost"; version = "5.0.17"; sha256 = "1gnzrqdp26d7pwwz29gm4qb09n2zsb767qkhbwkifcsyxlwi6m0f"; })
|
||||
(fetchNuGet { pname = "runtime.win-x86.Microsoft.NETCore.DotNetHostPolicy"; version = "5.0.17"; sha256 = "089jww13gaf7x7yd9d3qkyx9iq8abcp3r147hd9nblh561c9bzbg"; })
|
||||
(fetchNuGet { pname = "runtime.win-x86.Microsoft.NETCore.DotNetHostResolver"; version = "5.0.17"; sha256 = "1nycl1rayk0fhaakpj6q9rfp2lv3dpl7pziavmd9kcfryz952ff5"; })
|
||||
];
|
||||
};
|
||||
}
|
|
@ -21,11 +21,11 @@
|
|||
}:
|
||||
|
||||
let
|
||||
version = "8.48.0.53";
|
||||
openjdk = "8.0.265";
|
||||
version = "8.68.0.19";
|
||||
openjdk = "8.0.362";
|
||||
|
||||
sha256_linux = "ed32513524b32a83b3b388831c69d1884df5675bd5069c6d1485fd1a060be209";
|
||||
sha256_darwin = "36f189bfbd0255195848835819377474ba9c1c868e3c204633c451c96e21f30a";
|
||||
sha256_linux = "sha256-jNty0iJoXG+sp7v2fGCrwZWCSZfQ4tkYe8ERixQMKL0=";
|
||||
sha256_darwin = "sha256-3/P3puM6a7tCHP5eZM6IzbdPrqnhY1dTa7QWss9M08M=";
|
||||
|
||||
platform = if stdenv.isDarwin then "macosx" else "linux";
|
||||
hash = if stdenv.isDarwin then sha256_darwin else sha256_linux;
|
||||
|
|
|
@ -22,12 +22,12 @@
|
|||
}:
|
||||
|
||||
let
|
||||
version = "11.52.13";
|
||||
openjdk = "11.0.13";
|
||||
version = "11.62.17";
|
||||
openjdk = "11.0.18";
|
||||
|
||||
sha256_x64_linux = "77a126669b26b3a89e0117b0f28cddfcd24fcd7699b2c1d35f921487148b9a9f";
|
||||
sha256_x64_darwin = "a96f9f859350f977319ebb5c2a999c182ab6b99b24c60e19d97c54367868a63e";
|
||||
sha256_aarch64_darwin = "dmzfergSUVz39T30PT/6ZtT8JNqv5lzdX7zUsXsFGJg=";
|
||||
sha256_x64_linux = "sha256-b65oEbDzrrsUw+WaX94USBz/QS74yiMiGZPxqzMmmqs=";
|
||||
sha256_x64_darwin = "sha256-nRRWTWiog8bRblmmPIPE5YibA34St3ZrJpZN91qEDUg=";
|
||||
sha256_aarch64_darwin = "sha256-TBTrBxOfGo6MV+Md49P3sDfqVG1e+NraqfVbw9WTppk=";
|
||||
|
||||
platform = if stdenv.isDarwin then "macosx" else "linux";
|
||||
hash = if stdenv.isAarch64 && stdenv.isDarwin then sha256_aarch64_darwin else if stdenv.isDarwin then sha256_x64_darwin else sha256_x64_linux;
|
||||
|
|
|
@ -1,10 +1,10 @@
|
|||
{ lib, mkCoqDerivation, coq, StructTact, version ? null }:
|
||||
|
||||
with lib; mkCoqDerivation {
|
||||
mkCoqDerivation {
|
||||
pname = "cheerios";
|
||||
owner = "uwplse";
|
||||
inherit version;
|
||||
defaultVersion = if versions.range "8.6" "8.16" coq.version then "20200201" else null;
|
||||
defaultVersion = if lib.versions.range "8.6" "8.16" coq.version then "20200201" else null;
|
||||
release."20200201".rev = "9c7f66e57b91f706d70afa8ed99d64ed98ab367d";
|
||||
release."20200201".sha256 = "1h55s6lk47bk0lv5ralh81z55h799jbl9mhizmqwqzy57y8wqgs1";
|
||||
|
||||
|
|
|
@ -1,10 +1,10 @@
|
|||
{ lib, mkCoqDerivation, coq, bignums, version ? null }:
|
||||
|
||||
with lib; mkCoqDerivation {
|
||||
mkCoqDerivation {
|
||||
pname = "color";
|
||||
owner = "fblanqui";
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch coq.version [
|
||||
defaultVersion = with lib.versions; lib.switch coq.version [
|
||||
{case = range "8.12" "8.16"; out = "1.8.2"; }
|
||||
{case = range "8.10" "8.11"; out = "1.7.0"; }
|
||||
{case = range "8.8" "8.9"; out = "1.6.0"; }
|
||||
|
@ -26,6 +26,6 @@ with lib; mkCoqDerivation {
|
|||
meta = {
|
||||
homepage = "https://github.com/fblanqui/color";
|
||||
description = "CoLoR is a library of formal mathematical definitions and proofs of theorems on rewriting theory and termination whose correctness has been mechanically checked by the Coq proof assistant.";
|
||||
maintainers = with maintainers; [ jpas jwiegley ];
|
||||
maintainers = with lib.maintainers; [ jpas jwiegley ];
|
||||
};
|
||||
}
|
||||
|
|
|
@ -1,11 +1,11 @@
|
|||
{ lib, mkCoqDerivation, autoconf, automake, coq, version ? null }:
|
||||
|
||||
with lib; mkCoqDerivation {
|
||||
mkCoqDerivation {
|
||||
pname = "HoTT";
|
||||
repo = "Coq-HoTT";
|
||||
owner = "HoTT";
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch coq.coq-version [
|
||||
defaultVersion = with lib.versions; lib.switch coq.coq-version [
|
||||
{ case = range "8.14" "8.16"; out = coq.coq-version; }
|
||||
] null;
|
||||
releaseRev = v: "V${v}";
|
||||
|
@ -20,6 +20,6 @@ with lib; mkCoqDerivation {
|
|||
meta = {
|
||||
homepage = "https://homotopytypetheory.org/";
|
||||
description = "Homotopy type theory";
|
||||
maintainers = with maintainers; [ siddharthist ];
|
||||
maintainers = with lib.maintainers; [ siddharthist ];
|
||||
};
|
||||
}
|
||||
|
|
|
@ -1,10 +1,10 @@
|
|||
{ lib, mkCoqDerivation, coq, version ? null , paco, coq-ext-lib }:
|
||||
|
||||
with lib; mkCoqDerivation rec {
|
||||
mkCoqDerivation rec {
|
||||
pname = "InteractionTrees";
|
||||
owner = "DeepSpec";
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch coq.version [
|
||||
defaultVersion = with lib.versions; lib.switch coq.version [
|
||||
{ case = range "8.10" "8.16"; out = "4.0.0"; }
|
||||
] null;
|
||||
release."4.0.0".sha256 = "0h5rhndl8syc24hxq1gch86kj7mpmgr89bxp2hmf28fd7028ijsm";
|
||||
|
@ -12,6 +12,6 @@ with lib; mkCoqDerivation rec {
|
|||
propagatedBuildInputs = [ coq-ext-lib paco ];
|
||||
meta = {
|
||||
description = "A Library for Representing Recursive and Impure Programs in Coq";
|
||||
maintainers = with maintainers; [ larsr ];
|
||||
maintainers = with lib.maintainers; [ larsr ];
|
||||
};
|
||||
}
|
||||
|
|
|
@ -1,11 +1,10 @@
|
|||
{ lib, mkCoqDerivation, coq, version ? null }:
|
||||
|
||||
with lib;
|
||||
mkCoqDerivation {
|
||||
pname = "LibHyps";
|
||||
owner = "Matafou";
|
||||
inherit version;
|
||||
defaultVersion = if (versions.range "8.11" "8.16") coq.version then "2.0.4.1" else null;
|
||||
defaultVersion = if (lib.versions.range "8.11" "8.16") coq.version then "2.0.4.1" else null;
|
||||
release = {
|
||||
"2.0.4.1".sha256 = "09p89701zhrfdmqlpxw3mziw8yylj1w1skb4b0xpbdwd1vsn4k3h";
|
||||
};
|
||||
|
@ -16,6 +15,6 @@ mkCoqDerivation {
|
|||
|
||||
meta = {
|
||||
description = "Hypotheses manipulation library";
|
||||
license = licenses.mit;
|
||||
license = lib.licenses.mit;
|
||||
};
|
||||
}
|
||||
|
|
|
@ -1,10 +1,10 @@
|
|||
{ lib, mkCoqDerivation, coq, version ? null }:
|
||||
|
||||
with lib; mkCoqDerivation {
|
||||
mkCoqDerivation {
|
||||
pname = "StructTact";
|
||||
owner = "uwplse";
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch coq.coq-version [
|
||||
defaultVersion = with lib.versions; lib.switch coq.coq-version [
|
||||
{ case = range "8.6" "8.16"; out = "20210328"; }
|
||||
{ case = range "8.5" "8.13"; out = "20181102"; }
|
||||
] null;
|
||||
|
|
|
@ -1,7 +1,5 @@
|
|||
{ lib, mkCoqDerivation, coq, compcert, ITree, version ? null }:
|
||||
|
||||
with lib;
|
||||
|
||||
# A few modules that are not built and installed by default
|
||||
# but that may be useful to some users.
|
||||
# They depend on ITree.
|
||||
|
@ -11,7 +9,7 @@ let extra_floyd_files = [
|
|||
"powerlater.v"
|
||||
]
|
||||
# floyd/printf.v is broken in VST 2.9
|
||||
++ optional (!versions.isGe "8.13" coq.coq-version) "printf.v"
|
||||
++ lib.optional (!lib.versions.isGe "8.13" coq.coq-version) "printf.v"
|
||||
++ [
|
||||
"quickprogram.v"
|
||||
];
|
||||
|
@ -24,7 +22,7 @@ mkCoqDerivation {
|
|||
owner = "PrincetonUniversity";
|
||||
repo = "VST";
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch coq.coq-version [
|
||||
defaultVersion = with lib.versions; lib.switch coq.coq-version [
|
||||
{ case = range "8.15" "8.16"; out = "2.11.1"; }
|
||||
{ case = range "8.14" "8.16"; out = "2.10"; }
|
||||
{ case = range "8.13" "8.15"; out = "2.9"; }
|
||||
|
|
|
@ -1,10 +1,10 @@
|
|||
{ lib, mkCoqDerivation, coq, version ? null }:
|
||||
|
||||
with lib; mkCoqDerivation {
|
||||
mkCoqDerivation {
|
||||
pname = "Velisarios";
|
||||
owner = "vrahli";
|
||||
inherit version;
|
||||
defaultVersion = if versions.range "8.6" "8.8" coq.coq-version then "20180221" else null;
|
||||
defaultVersion = if lib.versions.range "8.6" "8.8" coq.coq-version then "20180221" else null;
|
||||
|
||||
release."20180221".rev = "e1eee1f10d5d46331a560bd8565ac101229d0d6b";
|
||||
release."20180221".sha256 = "0l9885nxy0n955fj1gnijlxl55lyxiv9yjfmz8hmfrn9hl8vv1m2";
|
||||
|
|
|
@ -1,11 +1,11 @@
|
|||
{ lib, mkCoqDerivation, coq, Cheerios, InfSeqExt, ssreflect, version ? null }:
|
||||
|
||||
|
||||
with lib; mkCoqDerivation {
|
||||
mkCoqDerivation {
|
||||
pname = "verdi";
|
||||
owner = "uwplse";
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch coq.coq-version [
|
||||
defaultVersion = with lib.versions; lib.switch coq.coq-version [
|
||||
{ case = range "8.7" "8.16"; out = "20211026"; }
|
||||
{ case = range "8.7" "8.14"; out = "20210524"; }
|
||||
{ case = range "8.7" "8.13"; out = "20200131"; }
|
||||
|
|
|
@ -1,5 +1,4 @@
|
|||
{ lib, mkCoqDerivation, coq, version ? null }:
|
||||
with lib;
|
||||
|
||||
mkCoqDerivation {
|
||||
pname = "aac-tactics";
|
||||
|
@ -21,7 +20,7 @@ mkCoqDerivation {
|
|||
release."8.5.0".sha256 = "sha256-7yNxJn6CH5xS5w/zsXfcZYORa6e5/qS9v8PUq2o02h4=";
|
||||
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch coq.coq-version [
|
||||
defaultVersion = with lib.versions; lib.switch coq.coq-version [
|
||||
{ case = "8.16"; out = "8.16.0"; }
|
||||
{ case = "8.15"; out = "8.15.1"; }
|
||||
{ case = "8.14"; out = "8.14.1"; }
|
||||
|
@ -37,7 +36,7 @@ mkCoqDerivation {
|
|||
|
||||
mlPlugin = true;
|
||||
|
||||
meta = {
|
||||
meta = with lib; {
|
||||
description = "Coq plugin providing tactics for rewriting universally quantified equations";
|
||||
longDescription = ''
|
||||
This Coq plugin provides tactics for rewriting universally quantified
|
||||
|
|
|
@ -1,6 +1,5 @@
|
|||
{ lib, mkCoqDerivation, coq, mathcomp-ssreflect, mathcomp-algebra, mathcomp-fingroup, paramcoq
|
||||
, version ? null }:
|
||||
with lib;
|
||||
|
||||
mkCoqDerivation {
|
||||
pname = "addition-chains";
|
||||
|
@ -12,7 +11,7 @@ mkCoqDerivation {
|
|||
releaseRev = (v: "v${v}");
|
||||
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch coq.coq-version [
|
||||
defaultVersion = with lib.versions; lib.switch coq.coq-version [
|
||||
{ case = range "8.13" "8.16"; out = "0.6"; }
|
||||
{ case = range "8.11" "8.12"; out = "0.4"; }
|
||||
] null;
|
||||
|
@ -21,7 +20,7 @@ mkCoqDerivation {
|
|||
|
||||
useDune = true;
|
||||
|
||||
meta = {
|
||||
meta = with lib; {
|
||||
description = "Exponentiation algorithms following addition chains";
|
||||
longDescription = ''
|
||||
Addition chains are algorithms for computations of the p-th
|
||||
|
|
|
@ -1,5 +1,4 @@
|
|||
{ lib, mkCoqDerivation, coq, mathcomp-ssreflect, version ? null }:
|
||||
with lib;
|
||||
|
||||
mkCoqDerivation {
|
||||
pname = "autosubst";
|
||||
|
@ -8,13 +7,13 @@ mkCoqDerivation {
|
|||
release."1.7".sha256 = "sha256-qoyteQ5W2Noxf12uACOVeHhPLvgmTzrvEo6Ts+FKTGI=";
|
||||
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch coq.coq-version [
|
||||
defaultVersion = with lib.versions; lib.switch coq.coq-version [
|
||||
{ case = range "8.10" "8.16"; out = "1.7"; }
|
||||
] null;
|
||||
|
||||
propagatedBuildInputs = [ mathcomp-ssreflect ];
|
||||
|
||||
meta = {
|
||||
meta = with lib; {
|
||||
homepage = "https://www.ps.uni-saarland.de/autosubst/";
|
||||
description = "Automation for de Bruijn syntax and substitution in Coq";
|
||||
maintainers = with maintainers; [ siraben jwiegley ];
|
||||
|
|
|
@ -1,11 +1,11 @@
|
|||
{ lib, mkCoqDerivation, coq, version ? null }:
|
||||
|
||||
with lib; mkCoqDerivation {
|
||||
mkCoqDerivation {
|
||||
pname = "bignums";
|
||||
owner = "coq";
|
||||
displayVersion = { bignums = ""; };
|
||||
inherit version;
|
||||
defaultVersion = if versions.isGe "8.6" coq.coq-version
|
||||
defaultVersion = if lib.versions.isGe "8.6" coq.coq-version
|
||||
then "${coq.coq-version}.0" else null;
|
||||
|
||||
release."8.17.0".sha256 = "sha256-MXYjqN86+3O4hT2ql62U83T5H03E/8ysH8erpvC/oyw=";
|
||||
|
@ -25,5 +25,5 @@ with lib; mkCoqDerivation {
|
|||
|
||||
mlPlugin = true;
|
||||
|
||||
meta = { license = licenses.lgpl2; };
|
||||
meta = { license = lib.licenses.lgpl2; };
|
||||
}
|
||||
|
|
|
@ -1,6 +1,6 @@
|
|||
{ lib, mkCoqDerivation, coq, ssreflect, equations, version ? null }:
|
||||
|
||||
with lib; mkCoqDerivation {
|
||||
mkCoqDerivation {
|
||||
|
||||
pname = "category-theory";
|
||||
owner = "jwiegley";
|
||||
|
@ -16,7 +16,7 @@ with lib; mkCoqDerivation {
|
|||
release."20180709".sha256 = "0f2nr8dgn1ab7hr7jrdmr1zla9g9h8216q4yf4wnff9qkln8sbbs";
|
||||
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch coq.coq-version [
|
||||
defaultVersion = with lib.versions; lib.switch coq.coq-version [
|
||||
{ case = range "8.14" "8.16"; out = "1.0.0"; }
|
||||
{ case = range "8.10" "8.15"; out = "20211213"; }
|
||||
{ case = range "8.8" "8.9"; out = "20190414"; }
|
||||
|
@ -28,6 +28,6 @@ with lib; mkCoqDerivation {
|
|||
|
||||
meta = {
|
||||
description = "A formalization of category theory in Coq for personal study and practical work";
|
||||
maintainers = with maintainers; [ jwiegley ];
|
||||
maintainers = with lib.maintainers; [ jwiegley ];
|
||||
};
|
||||
}
|
||||
|
|
|
@ -1,6 +1,5 @@
|
|||
{ lib, mkCoqDerivation, coq, version ? null }:
|
||||
|
||||
with lib;
|
||||
mkCoqDerivation {
|
||||
|
||||
pname = "ceres";
|
||||
|
@ -8,10 +7,10 @@ mkCoqDerivation {
|
|||
owner = "Lysxia";
|
||||
|
||||
inherit version;
|
||||
defaultVersion = if versions.range "8.8" "8.16" coq.version then "0.4.0" else null;
|
||||
defaultVersion = if lib.versions.range "8.8" "8.16" coq.version then "0.4.0" else null;
|
||||
release."0.4.0".sha256 = "sha256:0zwp3pn6fdj0qdig734zdczrls886al06mxqhhabms0jvvqijmbi";
|
||||
|
||||
meta = {
|
||||
meta = with lib; {
|
||||
description = "Library for serialization to S-expressions";
|
||||
license = licenses.mit;
|
||||
maintainers = with maintainers; [ Zimmi48 ];
|
||||
|
|
|
@ -5,8 +5,6 @@
|
|||
, version ? null
|
||||
}:
|
||||
|
||||
with lib;
|
||||
|
||||
let compcert = mkCoqDerivation rec {
|
||||
|
||||
pname = "compcert";
|
||||
|
@ -15,7 +13,7 @@ let compcert = mkCoqDerivation rec {
|
|||
inherit version;
|
||||
releaseRev = v: "v${v}";
|
||||
|
||||
defaultVersion = with versions; switch coq.version [
|
||||
defaultVersion = with lib.versions; lib.switch coq.version [
|
||||
{ case = range "8.14" "8.16"; out = "3.11"; }
|
||||
{ case = isEq "8.13" ; out = "3.10"; }
|
||||
{ case = isEq "8.12" ; out = "3.9"; }
|
||||
|
@ -84,7 +82,7 @@ let compcert = mkCoqDerivation rec {
|
|||
}; in
|
||||
compcert.overrideAttrs (o:
|
||||
{
|
||||
patches = with versions; switch [ coq.version o.version ] [
|
||||
patches = with lib.versions; lib.switch [ coq.version o.version ] [
|
||||
{ cases = [ (range "8.12.2" "8.13.2") "3.8" ];
|
||||
out = [
|
||||
# Support for Coq 8.12.2
|
||||
|
|
|
@ -1,16 +1,16 @@
|
|||
{ lib, mkCoqDerivation, coq, callPackage }:
|
||||
|
||||
with lib; let mkContrib = pname: coqs: param:
|
||||
let mkContrib = pname: coqs: param:
|
||||
let contribVersion = {version ? null}: mkCoqDerivation ({
|
||||
inherit pname version;
|
||||
owner = "coq-contribs";
|
||||
mlPlugin = true;
|
||||
} // optionalAttrs (builtins.elem coq.coq-version coqs) ({
|
||||
} // lib.optionalAttrs (builtins.elem coq.coq-version coqs) ({
|
||||
defaultVersion = param.version;
|
||||
release = { "${param.version}" = { inherit (param) rev sha256; }; };
|
||||
} // (removeAttrs param [ "version" "rev" "sha256" ]))
|
||||
); in
|
||||
makeOverridable contribVersion {} ; in
|
||||
lib.makeOverridable contribVersion {} ; in
|
||||
{
|
||||
aac-tactics = mkContrib "aac-tactics" [ "8.7" "8.8" ] {
|
||||
"8.7" = {
|
||||
|
|
|
@ -1,10 +1,10 @@
|
|||
{ lib, mkCoqDerivation, coq, mathcomp-algebra, version ? null }:
|
||||
|
||||
with lib; mkCoqDerivation {
|
||||
mkCoqDerivation {
|
||||
pname = "coq-bits";
|
||||
repo = "bits";
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch coq.coq-version [
|
||||
defaultVersion = with lib.versions; lib.switch coq.coq-version [
|
||||
{ case = range "8.10" "8.16"; out = "1.1.0"; }
|
||||
{ case = range "8.7" "8.15"; out = "1.0.0"; }
|
||||
] null;
|
||||
|
@ -14,7 +14,7 @@ with lib; mkCoqDerivation {
|
|||
|
||||
propagatedBuildInputs = [ mathcomp-algebra ];
|
||||
|
||||
meta = {
|
||||
meta = with lib; {
|
||||
description = "A formalization of bitset operations in Coq";
|
||||
license = licenses.asl20;
|
||||
maintainers = with maintainers; [ ptival ];
|
||||
|
|
|
@ -1,10 +1,10 @@
|
|||
{ lib, mkCoqDerivation, coq, version ? null }:
|
||||
|
||||
with lib; mkCoqDerivation rec {
|
||||
mkCoqDerivation rec {
|
||||
pname = "coq-ext-lib";
|
||||
owner = "coq-ext-lib";
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch coq.coq-version [
|
||||
defaultVersion = with lib.versions; lib.switch coq.coq-version [
|
||||
{ case = range "8.11" "8.16"; out = "0.11.7"; }
|
||||
{ case = range "8.8" "8.16"; out = "0.11.6"; }
|
||||
{ case = range "8.8" "8.14"; out = "0.11.4"; }
|
||||
|
@ -30,6 +30,6 @@ with lib; mkCoqDerivation rec {
|
|||
|
||||
meta = {
|
||||
description = "A collection of theories and plugins that may be useful in other Coq developments";
|
||||
maintainers = with maintainers; [ jwiegley ptival ];
|
||||
maintainers = with lib.maintainers; [ jwiegley ptival ];
|
||||
};
|
||||
}
|
||||
|
|
|
@ -1,11 +1,11 @@
|
|||
{ lib, mkCoqDerivation, coq, ssreflect, version ? null }:
|
||||
|
||||
with lib; mkCoqDerivation {
|
||||
mkCoqDerivation {
|
||||
|
||||
pname = "coq-haskell";
|
||||
owner = "jwiegley";
|
||||
inherit version;
|
||||
defaultVersion = if versions.range "8.5" "8.8" coq.coq-version then "20171215" else null;
|
||||
defaultVersion = if lib.versions.range "8.5" "8.8" coq.coq-version then "20171215" else null;
|
||||
release."20171215".rev = "e2cf8b270c2efa3b56fab1ef6acc376c2c3de968";
|
||||
release."20171215".sha256 = "09dq1vvshhlhgjccrhqgbhnq2hrys15xryfszqq11rzpgvl2zgdv";
|
||||
|
||||
|
@ -16,6 +16,6 @@ with lib; mkCoqDerivation {
|
|||
|
||||
meta = {
|
||||
description = "A library for formalizing Haskell types and functions in Coq";
|
||||
maintainers = with maintainers; [ jwiegley ];
|
||||
maintainers = with lib.maintainers; [ jwiegley ];
|
||||
};
|
||||
}
|
||||
|
|
|
@ -1,10 +1,10 @@
|
|||
{ lib, mkCoqDerivation, coq, version ? null }:
|
||||
|
||||
with lib; mkCoqDerivation rec {
|
||||
mkCoqDerivation rec {
|
||||
pname = "coq-record-update";
|
||||
owner = "tchajed";
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch coq.coq-version [
|
||||
defaultVersion = with lib.versions; lib.switch coq.coq-version [
|
||||
{ case = range "8.10" "8.16"; out = "0.3.1"; }
|
||||
] null;
|
||||
release."0.3.1".sha256 = "sha256-DyGxO2tqmYZZluXN6Oy5Tw6fuLMyuyxonj8CCToWKkk=";
|
||||
|
@ -13,6 +13,6 @@ with lib; mkCoqDerivation rec {
|
|||
buildFlags = [ "NO_TEST=1" ];
|
||||
meta = {
|
||||
description = "Library to create Coq record update functions";
|
||||
maintainers = with maintainers; [ ineol ];
|
||||
maintainers = with lib.maintainers; [ ineol ];
|
||||
};
|
||||
}
|
||||
|
|
|
@ -2,14 +2,12 @@
|
|||
mathcomp-real-closed,
|
||||
lib, version ? null }:
|
||||
|
||||
with lib;
|
||||
|
||||
(mkCoqDerivation {
|
||||
|
||||
pname = "CoqEAL";
|
||||
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch [ coq.version mathcomp.version ] [
|
||||
defaultVersion = with lib.versions; lib.switch [ coq.version mathcomp.version ] [
|
||||
{ cases = [ (range "8.13" "8.16") (isGe "1.13.0") ]; out = "1.1.1"; }
|
||||
{ cases = [ (range "8.10" "8.15") (isGe "1.12.0") ]; out = "1.1.0"; }
|
||||
{ cases = [ (isGe "8.10") (range "1.11.0" "1.12.0") ]; out = "1.0.5"; }
|
||||
|
@ -28,9 +26,9 @@ with lib;
|
|||
|
||||
meta = {
|
||||
description = "CoqEAL - The Coq Effective Algebra Library";
|
||||
license = licenses.mit;
|
||||
license = lib.licenses.mit;
|
||||
};
|
||||
}).overrideAttrs (o: {
|
||||
propagatedBuildInputs = o.propagatedBuildInputs
|
||||
++ optional (versions.isGe "1.1" o.version || o.version == "dev") mathcomp-real-closed;
|
||||
++ lib.optional (lib.versions.isGe "1.1" o.version || o.version == "dev") mathcomp-real-closed;
|
||||
})
|
||||
|
|
|
@ -1,10 +1,10 @@
|
|||
{ lib, mkCoqDerivation, coq, version ? null }:
|
||||
|
||||
with lib; mkCoqDerivation {
|
||||
mkCoqDerivation {
|
||||
inherit version;
|
||||
pname = "coqhammer";
|
||||
owner = "lukaszcz";
|
||||
defaultVersion = with versions; switch coq.coq-version [
|
||||
defaultVersion = with lib.versions; lib.switch coq.coq-version [
|
||||
{ case = "8.15"; out = "1.3.2-coq8.15"; }
|
||||
{ case = "8.14"; out = "1.3.2-coq8.14"; }
|
||||
{ case = "8.13"; out = "1.3.2-coq8.13"; }
|
||||
|
@ -57,7 +57,7 @@ with lib; mkCoqDerivation {
|
|||
|
||||
mlPlugin = true;
|
||||
|
||||
meta = {
|
||||
meta = with lib; {
|
||||
homepage = "http://cl-informatik.uibk.ac.at/cek/coqhammer/";
|
||||
description = "Automation for Dependent Type Theory";
|
||||
license = licenses.lgpl21;
|
||||
|
|
|
@ -8,14 +8,14 @@
|
|||
, coq
|
||||
, version ? null }:
|
||||
|
||||
with lib; mkCoqDerivation rec {
|
||||
mkCoqDerivation rec {
|
||||
pname = "coqide";
|
||||
inherit version;
|
||||
|
||||
inherit (coq) src;
|
||||
release."${coq.version}" = {};
|
||||
|
||||
defaultVersion = if versions.isGe "8.14" coq.version then coq.version else null;
|
||||
defaultVersion = if lib.versions.isGe "8.14" coq.version then coq.version else null;
|
||||
|
||||
preConfigure = ''
|
||||
patchShebangs dev/tools/
|
||||
|
|
|
@ -1,11 +1,11 @@
|
|||
{ which, lib, mkCoqDerivation, coq, bignums, version ? null }:
|
||||
|
||||
with lib; mkCoqDerivation {
|
||||
mkCoqDerivation {
|
||||
|
||||
pname = "coqprime";
|
||||
owner = "thery";
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch coq.coq-version [
|
||||
defaultVersion = with lib.versions; lib.switch coq.coq-version [
|
||||
{ case = range "8.12" "8.16"; out = "8.15"; }
|
||||
{ case = range "8.10" "8.11"; out = "8.10"; }
|
||||
{ case = range "8.8" "8.9"; out = "8.8"; }
|
||||
|
|
|
@ -1,12 +1,10 @@
|
|||
{ lib, mkCoqDerivation, coq, version ? null }:
|
||||
|
||||
with lib;
|
||||
|
||||
mkCoqDerivation {
|
||||
pname = "coqtail-math";
|
||||
owner = "coq-community";
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch coq.coq-version [
|
||||
defaultVersion = with lib.versions; lib.switch coq.coq-version [
|
||||
{ case = range "8.11" "8.15"; out = "8.14"; }
|
||||
{ case = range "8.11" "8.13"; out = "20201124"; }
|
||||
] null;
|
||||
|
@ -15,7 +13,7 @@ mkCoqDerivation {
|
|||
release."20201124".rev = "5c22c3d7dcd8cf4c47cf84a281780f5915488e9e";
|
||||
release."20201124".sha256 = "sha256-wd+Lh7dpAD4zfpyKuztDmSFEZo5ZiFrR8ti2jUCVvoQ=";
|
||||
mlPlugin = true;
|
||||
meta = {
|
||||
meta = with lib; {
|
||||
license = licenses.lgpl3Only;
|
||||
maintainers = [ maintainers.siraben ];
|
||||
};
|
||||
|
|
|
@ -1,12 +1,12 @@
|
|||
{ lib, mkCoqDerivation, autoconf,
|
||||
coq, ssreflect, version ? null }:
|
||||
|
||||
with lib; mkCoqDerivation {
|
||||
mkCoqDerivation {
|
||||
pname = "coquelicot";
|
||||
owner = "coquelicot";
|
||||
domain = "gitlab.inria.fr";
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch coq.coq-version [
|
||||
defaultVersion = with lib.versions; lib.switch coq.coq-version [
|
||||
{ case = range "8.8" "8.16"; out = "3.2.0"; }
|
||||
{ case = range "8.8" "8.13"; out = "3.1.0"; }
|
||||
{ case = range "8.5" "8.9"; out = "3.0.2"; }
|
||||
|
@ -20,7 +20,7 @@ with lib; mkCoqDerivation {
|
|||
propagatedBuildInputs = [ ssreflect ];
|
||||
useMelquiondRemake.logpath = "Coquelicot";
|
||||
|
||||
meta = {
|
||||
meta = with lib; {
|
||||
homepage = "http://coquelicot.saclay.inria.fr/";
|
||||
description = "A Coq library for Reals";
|
||||
license = licenses.lgpl3;
|
||||
|
|
|
@ -1,9 +1,9 @@
|
|||
{ lib, mkCoqDerivation, coq, bignums, math-classes, version ? null }:
|
||||
|
||||
with lib; mkCoqDerivation rec {
|
||||
mkCoqDerivation rec {
|
||||
pname = "corn";
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch coq.coq-version [
|
||||
defaultVersion = with lib.versions; lib.switch coq.coq-version [
|
||||
{ case = "8.6"; out = "8.8.1"; }
|
||||
{ case = (range "8.11" "8.16"); out = "8.16.0"; }
|
||||
{ case = (range "8.7" "8.15"); out = "8.13.0"; }
|
||||
|
@ -21,7 +21,7 @@ with lib; mkCoqDerivation rec {
|
|||
|
||||
propagatedBuildInputs = [ bignums math-classes ];
|
||||
|
||||
meta = {
|
||||
meta = with lib; {
|
||||
homepage = "http://c-corn.github.io/";
|
||||
license = licenses.gpl2;
|
||||
description = "A Coq library for constructive analysis";
|
||||
|
|
|
@ -1,14 +1,13 @@
|
|||
{ lib, mkCoqDerivation, coq, version ? null
|
||||
, ssreflect
|
||||
}:
|
||||
with lib;
|
||||
|
||||
mkCoqDerivation {
|
||||
pname = "deriving";
|
||||
owner = "arthuraa";
|
||||
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch coq.coq-version [
|
||||
defaultVersion = with lib.versions; lib.switch coq.coq-version [
|
||||
{ case = range "8.11" "8.16"; out = "0.1.0"; }
|
||||
] null;
|
||||
|
||||
|
@ -20,7 +19,7 @@ mkCoqDerivation {
|
|||
|
||||
mlPlugin = true;
|
||||
|
||||
meta = {
|
||||
meta = with lib; {
|
||||
description = "Generic instances of MathComp classes";
|
||||
license = licenses.mit;
|
||||
maintainers = [ maintainers.vbgl ];
|
||||
|
|
|
@ -1,14 +1,13 @@
|
|||
{ lib, mkCoqDerivation, autoreconfHook, coq, version ? null }:
|
||||
|
||||
with lib;
|
||||
let hasWarning = versionAtLeast coq.ocamlPackages.ocaml.version "4.08"; in
|
||||
let hasWarning = lib.versionAtLeast coq.ocamlPackages.ocaml.version "4.08"; in
|
||||
|
||||
mkCoqDerivation {
|
||||
pname = "dpdgraph";
|
||||
owner = "Karmaki";
|
||||
repo = "coq-dpdgraph";
|
||||
inherit version;
|
||||
defaultVersion = switch coq.coq-version [
|
||||
defaultVersion = lib.switch coq.coq-version [
|
||||
{ case = "8.16"; out = "1.0+8.16"; }
|
||||
{ case = "8.15"; out = "1.0+8.15"; }
|
||||
{ case = "8.14"; out = "1.0+8.14"; }
|
||||
|
@ -47,11 +46,11 @@ mkCoqDerivation {
|
|||
|
||||
# dpd_compute.ml uses deprecated Pervasives.compare
|
||||
# Versions prior to 0.6.5 do not have the WARN_ERR build flag
|
||||
preConfigure = optionalString hasWarning ''
|
||||
preConfigure = lib.optionalString hasWarning ''
|
||||
substituteInPlace Makefile.in --replace "-warn-error +a " ""
|
||||
'';
|
||||
|
||||
buildFlags = optional hasWarning "WARN_ERR=";
|
||||
buildFlags = lib.optional hasWarning "WARN_ERR=";
|
||||
|
||||
preInstall = ''
|
||||
mkdir -p $out/bin
|
||||
|
@ -59,7 +58,7 @@ mkCoqDerivation {
|
|||
|
||||
extraInstallFlags = [ "BINDIR=$(out)/bin" ];
|
||||
|
||||
meta = {
|
||||
meta = with lib; {
|
||||
description = "Build dependency graphs between Coq objects";
|
||||
license = licenses.lgpl21;
|
||||
maintainers = with maintainers; [ vbgl ];
|
||||
|
|
|
@ -1,11 +1,11 @@
|
|||
{ lib, mkCoqDerivation, coq, version ? null }:
|
||||
|
||||
with lib; (mkCoqDerivation {
|
||||
(mkCoqDerivation {
|
||||
pname = "equations";
|
||||
owner = "mattam82";
|
||||
repo = "Coq-Equations";
|
||||
inherit version;
|
||||
defaultVersion = switch coq.coq-version [
|
||||
defaultVersion = lib.switch coq.coq-version [
|
||||
{ case = "8.16"; out = "1.3+8.16"; }
|
||||
{ case = "8.15"; out = "1.3+8.15"; }
|
||||
{ case = "8.14"; out = "1.3+8.14"; }
|
||||
|
@ -57,11 +57,11 @@ with lib; (mkCoqDerivation {
|
|||
|
||||
mlPlugin = true;
|
||||
|
||||
meta = {
|
||||
meta = with lib; {
|
||||
homepage = "https://mattam82.github.io/Coq-Equations/";
|
||||
description = "A plugin for Coq to add dependent pattern-matching";
|
||||
maintainers = with maintainers; [ jwiegley ];
|
||||
};
|
||||
}).overrideAttrs (o: {
|
||||
preBuild = "coq_makefile -f _CoqProject -o Makefile${optionalString (versionAtLeast o.version "1.2.1" || o.version == "dev") ".coq"}";
|
||||
preBuild = "coq_makefile -f _CoqProject -o Makefile${lib.optionalString (lib.versionAtLeast o.version "1.2.1" || o.version == "dev") ".coq"}";
|
||||
})
|
||||
|
|
|
@ -2,14 +2,13 @@
|
|||
, ssreflect
|
||||
, deriving
|
||||
}:
|
||||
with lib;
|
||||
|
||||
(mkCoqDerivation {
|
||||
pname = "extructures";
|
||||
owner = "arthuraa";
|
||||
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch [coq.coq-version ssreflect.version] [
|
||||
defaultVersion = with lib.versions; lib.switch [coq.coq-version ssreflect.version] [
|
||||
{ cases = [(range "8.11" "8.16") (isGe "1.12.0") ]; out = "0.3.1"; }
|
||||
{ cases = [(range "8.11" "8.14") (isLe "1.12.0") ]; out = "0.3.0"; }
|
||||
{ cases = [(range "8.10" "8.12") (isLe "1.12.0") ]; out = "0.2.2"; }
|
||||
|
@ -23,7 +22,7 @@ with lib;
|
|||
|
||||
propagatedBuildInputs = [ ssreflect ];
|
||||
|
||||
meta = {
|
||||
meta = with lib; {
|
||||
description = "Finite data structures with extensional reasoning";
|
||||
license = licenses.mit;
|
||||
maintainers = [ maintainers.vbgl ];
|
||||
|
@ -31,5 +30,5 @@ with lib;
|
|||
|
||||
}).overrideAttrs (o: {
|
||||
propagatedBuildInputs = o.propagatedBuildInputs
|
||||
++ optional (versionAtLeast o.version "0.3.0") deriving;
|
||||
++ lib.optional (lib.versionAtLeast o.version "0.3.0") deriving;
|
||||
})
|
||||
|
|
|
@ -1,6 +1,6 @@
|
|||
{lib, mkCoqDerivation, coq, python27, version ? null }:
|
||||
|
||||
with lib; mkCoqDerivation rec {
|
||||
mkCoqDerivation rec {
|
||||
pname = "fiat";
|
||||
owner = "mit-plv";
|
||||
repo = "fiat";
|
||||
|
@ -29,6 +29,6 @@ with lib; mkCoqDerivation rec {
|
|||
meta = {
|
||||
homepage = "http://plv.csail.mit.edu/fiat/";
|
||||
description = "A library for the Coq proof assistant for synthesizing efficient correct-by-construction programs from declarative specifications";
|
||||
maintainers = with maintainers; [ jwiegley ];
|
||||
maintainers = with lib.maintainers; [ jwiegley ];
|
||||
};
|
||||
}
|
||||
|
|
|
@ -1,12 +1,12 @@
|
|||
{ lib, bash, autoconf, automake,
|
||||
mkCoqDerivation, coq, version ? null }:
|
||||
|
||||
with lib; mkCoqDerivation {
|
||||
mkCoqDerivation {
|
||||
pname = "flocq";
|
||||
owner = "flocq";
|
||||
domain = "gitlab.inria.fr";
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch coq.coq-version [
|
||||
defaultVersion = with lib.versions; lib.switch coq.coq-version [
|
||||
{ case = range "8.14" "8.16"; out = "4.1.0"; }
|
||||
{ case = range "8.7" "8.15"; out = "3.4.3"; }
|
||||
{ case = range "8.5" "8.8"; out = "2.6.1"; }
|
||||
|
@ -22,7 +22,7 @@ with lib; mkCoqDerivation {
|
|||
mlPlugin = true;
|
||||
useMelquiondRemake.logpath = "Flocq";
|
||||
|
||||
meta = {
|
||||
meta = with lib; {
|
||||
description = "A floating-point formalization for the Coq system";
|
||||
license = licenses.lgpl3;
|
||||
maintainers = with maintainers; [ jwiegley ];
|
||||
|
|
|
@ -1,5 +1,4 @@
|
|||
{ lib, mkCoqDerivation, coq, mathcomp, version ? null }:
|
||||
with lib;
|
||||
|
||||
mkCoqDerivation {
|
||||
pname = "fourcolor";
|
||||
|
@ -12,15 +11,15 @@ mkCoqDerivation {
|
|||
release."1.2.5".sha256 = "sha256-3qOPNCRjGK2UdHGMSqElpIXhAPVCklpeQgZwf9AFals=";
|
||||
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch [ coq.version mathcomp.version ] [
|
||||
defaultVersion = with lib.versions; lib.switch [ coq.version mathcomp.version ] [
|
||||
{ cases = [ (isGe "8.11") (isGe "1.12") ]; out = "1.2.5"; }
|
||||
{ cases = [ (isGe "8.11") (range "1.11" "1.14") ]; out = "1.2.4"; }
|
||||
{ cases = [ (isLe "8.13") (pred.inter (isGe "1.11.0") (isLt "1.13")) ]; out = "1.2.3"; }
|
||||
{ cases = [ (isLe "8.13") (lib.pred.inter (isGe "1.11.0") (isLt "1.13")) ]; out = "1.2.3"; }
|
||||
] null;
|
||||
|
||||
propagatedBuildInputs = [ mathcomp.algebra mathcomp.ssreflect mathcomp.fingroup ];
|
||||
|
||||
meta = {
|
||||
meta = with lib; {
|
||||
description = "Formal proof of the Four Color Theorem ";
|
||||
maintainers = with maintainers; [ siraben ];
|
||||
license = licenses.cecill-b;
|
||||
|
|
|
@ -1,7 +1,7 @@
|
|||
{ lib, mkCoqDerivation, coq, hydra-battles, gaia,
|
||||
mathcomp-zify, mathcomp, version ? null }:
|
||||
|
||||
with lib; mkCoqDerivation rec {
|
||||
mkCoqDerivation rec {
|
||||
pname = "gaia-hydras";
|
||||
repo = "hydra-battles";
|
||||
|
||||
|
@ -10,7 +10,7 @@ with lib; mkCoqDerivation rec {
|
|||
releaseRev = (v: "v${v}");
|
||||
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch [coq.coq-version mathcomp.version] [
|
||||
defaultVersion = with lib.versions; lib.switch [coq.coq-version mathcomp.version] [
|
||||
{ cases = [ (range "8.14" "8.16") (isGe "1.12.0") ]; out = "0.6"; }
|
||||
{ cases = [ (range "8.13" "8.14") (isGe "1.12.0") ]; out = "0.5"; }
|
||||
] null;
|
||||
|
@ -23,7 +23,7 @@ with lib; mkCoqDerivation rec {
|
|||
|
||||
useDune = true;
|
||||
|
||||
meta = {
|
||||
meta = with lib; {
|
||||
description = "Comparison between ordinals in Gaia and Hydra battles";
|
||||
longDescription = ''
|
||||
The Gaia and Hydra battles projects develop different notions of ordinals.
|
||||
|
|
|
@ -1,6 +1,6 @@
|
|||
{ lib, mkCoqDerivation, coq, mathcomp, version ? null }:
|
||||
|
||||
with lib; mkCoqDerivation {
|
||||
mkCoqDerivation {
|
||||
pname = "gaia";
|
||||
|
||||
release."1.11".sha256 = "sha256:0gwb0blf37sv9gb0qpn34dab71zdcx7jsnqm3j9p58qw65cgsqn5";
|
||||
|
@ -11,7 +11,7 @@ with lib; mkCoqDerivation {
|
|||
releaseRev = (v: "v${v}");
|
||||
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch [ coq.version mathcomp.version ] [
|
||||
defaultVersion = with lib.versions; lib.switch [ coq.version mathcomp.version ] [
|
||||
{ cases = [ (range "8.10" "8.16") (isGe "1.12.0") ]; out = "1.15"; }
|
||||
{ cases = [ (range "8.10" "8.12") "1.11.0" ]; out = "1.11"; }
|
||||
] null;
|
||||
|
@ -19,7 +19,7 @@ with lib; mkCoqDerivation {
|
|||
propagatedBuildInputs =
|
||||
[ mathcomp.ssreflect mathcomp.algebra mathcomp.fingroup ];
|
||||
|
||||
meta = {
|
||||
meta = with lib; {
|
||||
description = "Implementation of books from Bourbaki's Elements of Mathematics in Coq";
|
||||
maintainers = with maintainers; [ Zimmi48 ];
|
||||
license = licenses.mit;
|
||||
|
|
|
@ -1,12 +1,12 @@
|
|||
{ which, lib, mkCoqDerivation, autoconf, coq, flocq, version ? null }:
|
||||
|
||||
with lib; mkCoqDerivation {
|
||||
mkCoqDerivation {
|
||||
pname = "gappalib";
|
||||
repo = "coq";
|
||||
owner = "gappa";
|
||||
domain = "gitlab.inria.fr";
|
||||
inherit version;
|
||||
defaultVersion = if versions.range "8.8" "8.16" coq.coq-version then "1.5.2" else null;
|
||||
defaultVersion = if lib.versions.range "8.8" "8.16" coq.coq-version then "1.5.2" else null;
|
||||
release."1.5.2".sha256 = "sha256-A021Bhqz5r2CZBayfjIiWrCIfUlejcQAfbTmOaf6QTM=";
|
||||
release."1.5.1".sha256 = "1806bq1z6q5rq2ma7d5kfbqfyfr755hjg0dq7b2llry8fx9cxjsg";
|
||||
release."1.5.0".sha256 = "1i1c0gakffxqqqqw064cbvc243yl325hxd50jmczr6mk18igk41n";
|
||||
|
@ -19,7 +19,7 @@ with lib; mkCoqDerivation {
|
|||
propagatedBuildInputs = [ flocq ];
|
||||
useMelquiondRemake.logpath = "Gappa";
|
||||
|
||||
meta = {
|
||||
meta = with lib; {
|
||||
description = "Coq support library for Gappa";
|
||||
license = licenses.lgpl21;
|
||||
maintainers = [ maintainers.vbgl ];
|
||||
|
|
|
@ -1,5 +1,4 @@
|
|||
{ lib, mkCoqDerivation, coq, hydra-battles, pocklington, version ? null }:
|
||||
with lib;
|
||||
|
||||
mkCoqDerivation {
|
||||
pname = "goedel";
|
||||
|
@ -11,13 +10,13 @@ mkCoqDerivation {
|
|||
release."8.13.0".sha256 = "0sqqkmj6wsk4xmhrnqkhcsbsrqjzn2gnk67nqzgrmjpw5danz8y5";
|
||||
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch coq.coq-version [
|
||||
defaultVersion = with lib.versions; lib.switch coq.coq-version [
|
||||
{ case = range "8.11" "8.16"; out = "8.13.0"; }
|
||||
] null;
|
||||
|
||||
propagatedBuildInputs = [ hydra-battles pocklington ];
|
||||
|
||||
meta = {
|
||||
meta = with lib; {
|
||||
description = "The Gödel-Rosser 1st incompleteness theorem in Coq";
|
||||
maintainers = with maintainers; [ siraben ];
|
||||
license = licenses.mit;
|
||||
|
|
|
@ -1,8 +1,6 @@
|
|||
{ lib, mkCoqDerivation, coq, mathcomp-algebra, mathcomp-finmap, mathcomp-fingroup
|
||||
, hierarchy-builder, version ? null }:
|
||||
|
||||
with lib;
|
||||
|
||||
mkCoqDerivation {
|
||||
pname = "graph-theory";
|
||||
|
||||
|
@ -11,13 +9,13 @@ mkCoqDerivation {
|
|||
releaseRev = v: "v${v}";
|
||||
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch coq.coq-version [
|
||||
defaultVersion = with lib.versions; lib.switch coq.coq-version [
|
||||
{ case = range "8.13" "8.16"; out = "0.9"; }
|
||||
] null;
|
||||
|
||||
propagatedBuildInputs = [ mathcomp-algebra mathcomp-finmap mathcomp-fingroup hierarchy-builder ];
|
||||
|
||||
meta = {
|
||||
meta = with lib; {
|
||||
description = "Library of formalized graph theory results in Coq";
|
||||
longDescription = ''
|
||||
A library of formalized graph theory results, including various
|
||||
|
|
|
@ -5,13 +5,13 @@ let fetcher = {rev, repo, owner, sha256, domain, ...}:
|
|||
url = "https://${domain}/${owner}/${repo}/download/${repo}-${rev}.zip";
|
||||
inherit sha256;
|
||||
}; in
|
||||
with lib; mkCoqDerivation {
|
||||
mkCoqDerivation {
|
||||
pname = "heq";
|
||||
repo = "Heq";
|
||||
owner = "gil.hur";
|
||||
domain = "sf.snu.ac.kr";
|
||||
inherit version fetcher;
|
||||
defaultVersion = if versions.isLt "8.8" coq.coq-version then "0.92" else null;
|
||||
defaultVersion = if lib.versions.isLt "8.8" coq.coq-version then "0.92" else null;
|
||||
release."0.92".sha256 = "0cf8y6728n81wwlbpq3vi7l2dbzi7759klypld4gpsjjp1y1fj74";
|
||||
|
||||
mlPlugin = true;
|
||||
|
@ -22,6 +22,6 @@ with lib; mkCoqDerivation {
|
|||
meta = {
|
||||
homepage = "https://ropas.snu.ac.kr/~gil.hur/Heq/";
|
||||
description = "Heq : a Coq library for Heterogeneous Equality";
|
||||
maintainers = with maintainers; [ jwiegley ];
|
||||
maintainers = with lib.maintainers; [ jwiegley ];
|
||||
};
|
||||
}
|
||||
|
|
|
@ -1,10 +1,10 @@
|
|||
{ lib, mkCoqDerivation, coq, coq-elpi, version ? null }:
|
||||
|
||||
with lib; let hb = mkCoqDerivation {
|
||||
let hb = mkCoqDerivation {
|
||||
pname = "hierarchy-builder";
|
||||
owner = "math-comp";
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch coq.coq-version [
|
||||
defaultVersion = with lib.versions; lib.switch coq.coq-version [
|
||||
{ case = range "8.15" "8.16"; out = "1.4.0"; }
|
||||
{ case = range "8.13" "8.14"; out = "1.2.0"; }
|
||||
{ case = range "8.12" "8.13"; out = "1.1.0"; }
|
||||
|
@ -25,16 +25,16 @@ with lib; let hb = mkCoqDerivation {
|
|||
|
||||
extraInstallFlags = [ "VFILES=structures.v" ];
|
||||
|
||||
meta = {
|
||||
meta = with lib; {
|
||||
description = "High level commands to declare a hierarchy based on packed classes";
|
||||
maintainers = with maintainers; [ cohencyril siraben ];
|
||||
license = licenses.mit;
|
||||
};
|
||||
}; in
|
||||
hb.overrideAttrs (o:
|
||||
optionalAttrs (versions.isGe "1.2.0" o.version || o.version == "dev")
|
||||
lib.optionalAttrs (lib.versions.isGe "1.2.0" o.version || o.version == "dev")
|
||||
{ buildPhase = "make build"; }
|
||||
//
|
||||
optionalAttrs (versions.isGe "1.1.0" o.version || o.version == "dev")
|
||||
lib.optionalAttrs (lib.versions.isGe "1.1.0" o.version || o.version == "dev")
|
||||
{ installFlags = [ "DESTDIR=$(out)" ] ++ o.installFlags; }
|
||||
)
|
||||
|
|
|
@ -1,5 +1,4 @@
|
|||
{ lib, mkCoqDerivation, coq, equations, LibHyps, version ? null }:
|
||||
with lib;
|
||||
|
||||
(mkCoqDerivation {
|
||||
pname = "hydra-battles";
|
||||
|
@ -11,14 +10,14 @@ with lib;
|
|||
releaseRev = (v: "v${v}");
|
||||
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch coq.coq-version [
|
||||
defaultVersion = with lib.versions; lib.switch coq.coq-version [
|
||||
{ case = range "8.13" "8.16"; out = "0.6"; }
|
||||
{ case = range "8.11" "8.12"; out = "0.4"; }
|
||||
] null;
|
||||
|
||||
useDune = true;
|
||||
|
||||
meta = {
|
||||
meta = with lib; {
|
||||
description = "Exploration of some properties of Kirby and Paris' hydra battles, with the help of Coq";
|
||||
longDescription = ''
|
||||
An exploration of some properties of Kirby and Paris' hydra
|
||||
|
@ -33,5 +32,5 @@ with lib;
|
|||
};
|
||||
}).overrideAttrs(o:
|
||||
let inherit (o) version; in {
|
||||
propagatedBuildInputs = [ equations ] ++ optional (versions.isGe "0.6" version || version == "dev") LibHyps;
|
||||
propagatedBuildInputs = [ equations ] ++ lib.optional (lib.versions.isGe "0.6" version || version == "dev") LibHyps;
|
||||
})
|
||||
|
|
|
@ -1,11 +1,11 @@
|
|||
{ lib, mkCoqDerivation, coq, stdpp, version ? null }:
|
||||
|
||||
with lib; mkCoqDerivation rec {
|
||||
mkCoqDerivation rec {
|
||||
pname = "iris";
|
||||
domain = "gitlab.mpi-sws.org";
|
||||
owner = "iris";
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch coq.coq-version [
|
||||
defaultVersion = with lib.versions; lib.switch coq.coq-version [
|
||||
{ case = range "8.13" "8.16"; out = "4.0.0"; }
|
||||
{ case = range "8.12" "8.14"; out = "3.5.0"; }
|
||||
{ case = range "8.11" "8.13"; out = "3.4.0"; }
|
||||
|
@ -26,7 +26,7 @@ with lib; mkCoqDerivation rec {
|
|||
fi
|
||||
'';
|
||||
|
||||
meta = {
|
||||
meta = with lib; {
|
||||
description = "The Coq development of the Iris Project";
|
||||
license = licenses.bsd3;
|
||||
maintainers = [ maintainers.vbgl ];
|
||||
|
|
|
@ -1,5 +1,4 @@
|
|||
{ lib, mkCoqDerivation, coq, version ? null }:
|
||||
with lib;
|
||||
|
||||
mkCoqDerivation rec {
|
||||
pname = "itauto";
|
||||
|
@ -11,7 +10,7 @@ mkCoqDerivation rec {
|
|||
release."8.14.0".sha256 = "sha256:1k6pqhv4dwpkwg81f2rlfg40wh070ks1gy9r0ravm2zhsbxqcfc9";
|
||||
release."8.13+no".sha256 = "sha256-gXoxtLcHPoyjJkt7WqvzfCMCQlh6kL2KtCGe3N6RC/A=";
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch coq.coq-version [
|
||||
defaultVersion = with lib.versions; lib.switch coq.coq-version [
|
||||
{ case = isEq "8.16"; out = "8.16.0"; }
|
||||
{ case = isEq "8.15"; out = "8.15.0"; }
|
||||
{ case = isEq "8.14"; out = "8.14.0"; }
|
||||
|
@ -22,7 +21,7 @@ mkCoqDerivation rec {
|
|||
nativeBuildInputs = (with coq.ocamlPackages; [ ocamlbuild ]);
|
||||
enableParallelBuilding = false;
|
||||
|
||||
meta = {
|
||||
meta = with lib; {
|
||||
description = "A reflexive SAT solver parameterised by a leaf tactic and Nelson-Oppen support";
|
||||
maintainers = with maintainers; [ siraben ];
|
||||
license = licenses.gpl3Plus;
|
||||
|
|
|
@ -1,10 +1,10 @@
|
|||
{ lib, mkCoqDerivation, which, coq, version ? null }:
|
||||
|
||||
with lib; mkCoqDerivation {
|
||||
mkCoqDerivation {
|
||||
pname = "ltac2";
|
||||
owner = "coq";
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch coq.coq-version [
|
||||
defaultVersion = with lib.versions; lib.switch coq.coq-version [
|
||||
{ case = "8.10"; out = "0.3"; }
|
||||
{ case = "8.9"; out = "0.2"; }
|
||||
{ case = "8.8"; out = "0.1"; }
|
||||
|
@ -19,7 +19,7 @@ with lib; mkCoqDerivation {
|
|||
|
||||
mlPlugin = true;
|
||||
|
||||
meta = {
|
||||
meta = with lib; {
|
||||
description = "A robust and expressive tactic language for Coq";
|
||||
maintainers = [ maintainers.vbgl ];
|
||||
license = licenses.lgpl21;
|
||||
|
|
|
@ -1,10 +1,10 @@
|
|||
{ lib, mkCoqDerivation, coq, bignums, version ? null }:
|
||||
|
||||
with lib; mkCoqDerivation {
|
||||
mkCoqDerivation {
|
||||
|
||||
pname = "math-classes";
|
||||
inherit version;
|
||||
defaultVersion = if versions.range "8.6" "8.16" coq.coq-version then "8.15.0" else null;
|
||||
defaultVersion = if lib.versions.range "8.6" "8.16" coq.coq-version then "8.15.0" else null;
|
||||
release."8.12.0".sha256 = "14nd6a08zncrl5yg2gzk0xf4iinwq4hxnsgm4fyv07ydbkxfb425";
|
||||
release."8.13.0".sha256 = "1ln7ziivfbxzbdvlhbvyg3v30jgblncmwcsam6gg3d1zz6r7cbby";
|
||||
release."8.15.0".sha256 = "10w1hm537k6jx8a8vghq1yx12rsa0sjk2ipv3scgir71ln30hllw";
|
||||
|
@ -14,6 +14,6 @@ with lib; mkCoqDerivation {
|
|||
meta = {
|
||||
homepage = "https://math-classes.github.io";
|
||||
description = "A library of abstract interfaces for mathematical structures in Coq.";
|
||||
maintainers = with maintainers; [ siddharthist jwiegley ];
|
||||
maintainers = with lib.maintainers; [ siddharthist jwiegley ];
|
||||
};
|
||||
}
|
||||
|
|
|
@ -7,7 +7,7 @@ mkCoqDerivation {
|
|||
owner = "math-comp";
|
||||
|
||||
inherit version;
|
||||
defaultVersion = with lib; with versions; switch [ coq.version mathcomp.version ] [
|
||||
defaultVersion = with lib; with versions; lib.switch [ coq.version mathcomp.version ] [
|
||||
{ cases = [ (range "8.10" "8.16") (range "1.12.0" "1.15.0") ]; out = "1.2.1"; }
|
||||
{ cases = [ (range "8.10" "8.15") (range "1.12.0" "1.14.0") ]; out = "1.2.0"; }
|
||||
{ cases = [ (range "8.10" "8.14") (range "1.11.0" "1.12.0") ]; out = "1.1.2"; }
|
||||
|
|
|
@ -1,14 +1,14 @@
|
|||
{ lib, mkCoqDerivation, coq, mathcomp-algebra,
|
||||
coq-elpi, mathcomp-zify, version ? null }:
|
||||
|
||||
with lib; mkCoqDerivation {
|
||||
mkCoqDerivation {
|
||||
namePrefix = [ "coq" "mathcomp" ];
|
||||
pname = "algebra-tactics";
|
||||
owner = "math-comp";
|
||||
inherit version;
|
||||
|
||||
defaultVersion = with versions;
|
||||
switch [ coq.coq-version mathcomp-algebra.version ] [
|
||||
defaultVersion = with lib.versions;
|
||||
lib.switch [ coq.coq-version mathcomp-algebra.version ] [
|
||||
{ cases = [ (range "8.13" "8.16") (isGe "1.12") ]; out = "1.0.0"; }
|
||||
] null;
|
||||
|
||||
|
@ -18,6 +18,6 @@ with lib; mkCoqDerivation {
|
|||
|
||||
meta = {
|
||||
description = "Ring and field tactics for Mathematical Components";
|
||||
maintainers = with maintainers; [ cohencyril ];
|
||||
maintainers = with lib.maintainers; [ cohencyril ];
|
||||
};
|
||||
}
|
||||
|
|
|
@ -21,7 +21,7 @@ let
|
|||
release."0.3.1".sha256 = "1iad288yvrjv8ahl9v18vfblgqb1l5z6ax644w49w9hwxs93f2k8";
|
||||
release."0.2.3".sha256 = "0p9mr8g1qma6h10qf7014dv98ln90dfkwn76ynagpww7qap8s966";
|
||||
|
||||
defaultVersion = with versions; switch [ coq.version mathcomp.version ] [
|
||||
defaultVersion = with versions; lib.switch [ coq.version mathcomp.version ] [
|
||||
{ cases = [ (isGe "8.14") (isGe "1.13.0") ]; out = "0.5.3"; }
|
||||
{ cases = [ (isGe "8.14") (range "1.13" "1.15") ]; out = "0.5.2"; }
|
||||
{ cases = [ (isGe "8.13") (range "1.13" "1.14") ]; out = "0.5.1"; }
|
||||
|
@ -40,7 +40,7 @@ let
|
|||
classical-deps = [ mathcomp.algebra mathcomp-finmap hierarchy-builder ];
|
||||
analysis-deps = [ mathcomp.field mathcomp-bigenough ];
|
||||
intra-deps = if package == "single" then []
|
||||
else map mathcomp_ (head (splitList (pred.equal package) packages));
|
||||
else map mathcomp_ (head (splitList (lib.pred.equal package) packages));
|
||||
pkgpath = if package == "single" then "."
|
||||
else if package == "analysis" then "theories" else "${package}";
|
||||
pname = if package == "single" then "mathcomp-analysis-single"
|
||||
|
|
|
@ -1,6 +1,6 @@
|
|||
{ coq, mkCoqDerivation, mathcomp, lib, version ? null }:
|
||||
|
||||
with lib; mkCoqDerivation {
|
||||
mkCoqDerivation {
|
||||
|
||||
namePrefix = [ "coq" "mathcomp" ];
|
||||
pname = "bigenough";
|
||||
|
@ -11,7 +11,7 @@ with lib; mkCoqDerivation {
|
|||
"1.0.1".sha256 = "sha256:02f4dv4rz72liciwxb2k7acwx6lgqz4381mqyq5854p3nbyn06aw";
|
||||
};
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch coq.version [
|
||||
defaultVersion = with lib.versions; lib.switch coq.version [
|
||||
{ case = range "8.10" "8.16"; out = "1.0.1"; }
|
||||
{ case = range "8.5" "8.14"; out = "1.0.0"; }
|
||||
] null;
|
||||
|
@ -20,6 +20,6 @@ with lib; mkCoqDerivation {
|
|||
|
||||
meta = {
|
||||
description = "A small library to do epsilon - N reasonning";
|
||||
license = licenses.cecill-b;
|
||||
license = lib.licenses.cecill-b;
|
||||
};
|
||||
}
|
||||
|
|
|
@ -1,12 +1,12 @@
|
|||
{ coq, mkCoqDerivation, mathcomp, lib, version ? null }:
|
||||
|
||||
with lib; mkCoqDerivation {
|
||||
mkCoqDerivation {
|
||||
|
||||
namePrefix = [ "coq" "mathcomp" ];
|
||||
pname = "finmap";
|
||||
owner = "math-comp";
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch [ coq.version mathcomp.version ] [
|
||||
defaultVersion = with lib.versions; lib.switch [ coq.version mathcomp.version ] [
|
||||
{ cases = [ (range "8.13" "8.16") (isGe "1.12") ]; out = "1.5.2"; }
|
||||
{ cases = [ (isGe "8.10") (isGe "1.11") ]; out = "1.5.1"; }
|
||||
{ cases = [ (range "8.7" "8.11") "1.11.0" ]; out = "1.5.0"; }
|
||||
|
@ -33,6 +33,6 @@ with lib; mkCoqDerivation {
|
|||
|
||||
meta = {
|
||||
description = "A finset and finmap library";
|
||||
license = licenses.cecill-b;
|
||||
license = lib.licenses.cecill-b;
|
||||
};
|
||||
}
|
||||
|
|
|
@ -1,7 +1,7 @@
|
|||
{ coq, mkCoqDerivation, mathcomp, mathcomp-bigenough,
|
||||
lib, version ? null }:
|
||||
|
||||
with lib; mkCoqDerivation {
|
||||
mkCoqDerivation {
|
||||
|
||||
namePrefix = [ "coq" "mathcomp" ];
|
||||
pname = "real-closed";
|
||||
|
@ -17,7 +17,7 @@ with lib; mkCoqDerivation {
|
|||
"1.0.1".sha256 = "0j81gkjbza5vg89v4n9z598mfdbql416963rj4b8fzm7dp2r4rxg";
|
||||
};
|
||||
|
||||
defaultVersion = with versions; switch [ coq.version mathcomp.version ] [
|
||||
defaultVersion = with lib.versions; lib.switch [ coq.version mathcomp.version ] [
|
||||
{ cases = [ (isGe "8.13") (isGe "1.12.0") ]; out = "1.1.3"; }
|
||||
{ cases = [ (isGe "8.10") (isGe "1.12.0") ]; out = "1.1.2"; }
|
||||
{ cases = [ (isGe "8.7") "1.11.0" ]; out = "1.1.1"; }
|
||||
|
@ -37,6 +37,6 @@ with lib; mkCoqDerivation {
|
|||
|
||||
meta = {
|
||||
description = "Mathematical Components Library on real closed fields";
|
||||
license = licenses.cecill-c;
|
||||
license = lib.licenses.cecill-c;
|
||||
};
|
||||
}
|
||||
|
|
|
@ -1,14 +1,15 @@
|
|||
{ coq, mkCoqDerivation, mathcomp-ssreflect, mathcomp-fingroup,
|
||||
lib, version ? null }@args:
|
||||
with lib; mkCoqDerivation {
|
||||
|
||||
mkCoqDerivation {
|
||||
|
||||
namePrefix = [ "coq" "mathcomp" ];
|
||||
pname = "tarjan";
|
||||
owner = "math-comp";
|
||||
|
||||
inherit version;
|
||||
defaultVersion = with versions;
|
||||
switch [ coq.version mathcomp-ssreflect.version ] [{
|
||||
defaultVersion = with lib.versions;
|
||||
lib.switch [ coq.version mathcomp-ssreflect.version ] [{
|
||||
cases = [ (range "8.10" "8.16") (isGe "1.12.0") ]; out = "1.0.0";
|
||||
}] null;
|
||||
release."1.0.0".sha256 = "sha256:0r459r0makshzwlygw6kd4lpvdjc43b3x5y9aa8x77f2z5gymjq1";
|
||||
|
@ -17,6 +18,6 @@ with lib; mkCoqDerivation {
|
|||
|
||||
meta = {
|
||||
description = "Proofs of Tarjan and Kosaraju connected components algorithms";
|
||||
license = licenses.cecill-b;
|
||||
license = lib.licenses.cecill-b;
|
||||
};
|
||||
}
|
||||
|
|
|
@ -1,6 +1,5 @@
|
|||
{ coq, mkCoqDerivation, mathcomp, lib, version ? null }:
|
||||
|
||||
with lib;
|
||||
mkCoqDerivation {
|
||||
namePrefix = [ "coq" "mathcomp" ];
|
||||
pname = "word";
|
||||
|
@ -15,13 +14,13 @@ mkCoqDerivation {
|
|||
release."1.0".sha256 = "sha256:0703m97rnivcbc7vvbd9rl2dxs6l8n52cbykynw61c6w9rhxspcg";
|
||||
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch [ coq.version mathcomp.version ] [
|
||||
defaultVersion = with lib.versions; lib.switch [ coq.version mathcomp.version ] [
|
||||
{ cases = [ (range "8.12" "8.16") (isGe "1.12") ]; out = "2.0"; }
|
||||
] null;
|
||||
|
||||
propagatedBuildInputs = [ mathcomp.algebra mathcomp.ssreflect mathcomp.fingroup ];
|
||||
|
||||
meta = {
|
||||
meta = with lib; {
|
||||
description = "Yet Another Coq Library on Machine Words";
|
||||
maintainers = [ maintainers.vbgl ];
|
||||
license = licenses.mit;
|
||||
|
|
|
@ -1,14 +1,14 @@
|
|||
{ lib, mkCoqDerivation, coq, mathcomp-algebra, mathcomp-ssreflect, mathcomp-fingroup, version ? null }:
|
||||
|
||||
with lib; mkCoqDerivation rec {
|
||||
mkCoqDerivation rec {
|
||||
namePrefix = [ "coq" "mathcomp" ];
|
||||
pname = "zify";
|
||||
repo = "mczify";
|
||||
owner = "math-comp";
|
||||
inherit version;
|
||||
|
||||
defaultVersion = with versions;
|
||||
switch [ coq.coq-version mathcomp-algebra.version ] [
|
||||
defaultVersion = with lib.versions;
|
||||
lib.switch [ coq.coq-version mathcomp-algebra.version ] [
|
||||
{ cases = [ (range "8.13" "8.16") (isGe "1.12") ]; out = "1.1.0+1.12+8.13"; }
|
||||
] null;
|
||||
|
||||
|
@ -19,6 +19,6 @@ with lib; mkCoqDerivation rec {
|
|||
|
||||
meta = {
|
||||
description = "Micromega tactics for Mathematical Components";
|
||||
maintainers = with maintainers; [ cohencyril ];
|
||||
maintainers = with lib.maintainers; [ cohencyril ];
|
||||
};
|
||||
}
|
||||
|
|
|
@ -18,7 +18,7 @@ let
|
|||
repo = "math-comp";
|
||||
owner = "math-comp";
|
||||
withDoc = single && (args.withDoc or false);
|
||||
defaultVersion = with versions; switch coq.coq-version [
|
||||
defaultVersion = with versions; lib.switch coq.coq-version [
|
||||
{ case = range "8.14" "8.16"; out = "1.15.0"; }
|
||||
{ case = range "8.11" "8.15"; out = "1.14.0"; }
|
||||
{ case = range "8.11" "8.15"; out = "1.13.0"; }
|
||||
|
@ -50,7 +50,7 @@ let
|
|||
|
||||
mathcomp_ = package: let
|
||||
mathcomp-deps = if package == "single" then []
|
||||
else map mathcomp_ (head (splitList (pred.equal package) packages));
|
||||
else map mathcomp_ (head (splitList (lib.pred.equal package) packages));
|
||||
pkgpath = if package == "single" then "mathcomp" else "mathcomp/${package}";
|
||||
pname = if package == "single" then "mathcomp" else "mathcomp-${package}";
|
||||
pkgallMake = ''
|
||||
|
|
|
@ -5,7 +5,7 @@ with builtins // lib;
|
|||
let
|
||||
repo = "metacoq";
|
||||
owner = "MetaCoq";
|
||||
defaultVersion = with versions; switch coq.coq-version [
|
||||
defaultVersion = with versions; lib.switch coq.coq-version [
|
||||
{ case = "8.11"; out = "1.0-beta2-8.11"; }
|
||||
{ case = "8.12"; out = "1.0-beta2-8.12"; }
|
||||
# Do not provide 8.13 because it does not compile with equations 1.3 provided by default (only 1.2.3)
|
||||
|
@ -34,7 +34,7 @@ let
|
|||
|
||||
metacoq_ = package: let
|
||||
metacoq-deps = if package == "single" then []
|
||||
else map metacoq_ (head (splitList (pred.equal package) packages));
|
||||
else map metacoq_ (head (splitList (lib.pred.equal package) packages));
|
||||
pkgpath = if package == "single" then "./" else "./${package}";
|
||||
pname = if package == "all" then "metacoq" else "metacoq-${package}";
|
||||
pkgallMake = ''
|
||||
|
|
|
@ -1,10 +1,10 @@
|
|||
{ lib, mkCoqDerivation, coq, version ? null }:
|
||||
|
||||
with lib; mkCoqDerivation {
|
||||
mkCoqDerivation {
|
||||
pname = "metalib";
|
||||
owner = "plclub";
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch coq.coq-version [
|
||||
defaultVersion = with lib.versions; lib.switch coq.coq-version [
|
||||
{ case = range "8.14" "8.16"; out = "8.15"; }
|
||||
{ case = range "8.10" "8.13"; out = "8.10"; }
|
||||
] null;
|
||||
|
@ -14,7 +14,7 @@ with lib; mkCoqDerivation {
|
|||
|
||||
sourceRoot = "source/Metalib";
|
||||
|
||||
meta = {
|
||||
meta = with lib; {
|
||||
license = licenses.mit;
|
||||
maintainers = [ maintainers.jwiegley ];
|
||||
};
|
||||
|
|
|
@ -1,6 +1,6 @@
|
|||
{ coq, mkCoqDerivation, mathcomp, mathcomp-finmap, mathcomp-bigenough,
|
||||
lib, version ? null, useDune ? false }@args:
|
||||
with lib; mkCoqDerivation {
|
||||
mkCoqDerivation {
|
||||
|
||||
namePrefix = [ "coq" "mathcomp" ];
|
||||
pname = "multinomials";
|
||||
|
@ -8,7 +8,7 @@ with lib; mkCoqDerivation {
|
|||
owner = "math-comp";
|
||||
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch [ coq.version mathcomp.version ] [
|
||||
defaultVersion = with lib.versions; lib.switch [ coq.version mathcomp.version ] [
|
||||
{ cases = [ (isGe "8.10") (isGe "1.12.0") ]; out = "1.5.5"; }
|
||||
{ cases = [ (range "8.10" "8.12") "1.12.0" ]; out = "1.5.3"; }
|
||||
{ cases = [ (range "8.7" "8.12") "1.11.0" ]; out = "1.5.2"; }
|
||||
|
@ -31,7 +31,7 @@ with lib; mkCoqDerivation {
|
|||
"1.0".sha256 = "1qmbxp1h81cy3imh627pznmng0kvv37k4hrwi2faa101s6bcx55m";
|
||||
};
|
||||
|
||||
useDuneifVersion = v: versions.isGe "1.5.3" v || v == "dev";
|
||||
useDuneifVersion = v: lib.versions.isGe "1.5.3" v || v == "dev";
|
||||
|
||||
preConfigure = ''
|
||||
patchShebangs configure || true
|
||||
|
@ -42,7 +42,7 @@ with lib; mkCoqDerivation {
|
|||
|
||||
meta = {
|
||||
description = "A Coq/SSReflect Library for Monoidal Rings and Multinomials";
|
||||
license = licenses.cecill-c;
|
||||
license = lib.licenses.cecill-c;
|
||||
};
|
||||
}
|
||||
// optionalAttrs (args?useDune) { inherit useDune; }
|
||||
// lib.optionalAttrs (args?useDune) { inherit useDune; }
|
||||
|
|
|
@ -1,5 +1,4 @@
|
|||
{ lib, mkCoqDerivation, mathcomp, version ? null }:
|
||||
with lib;
|
||||
|
||||
mkCoqDerivation {
|
||||
pname = "odd-order";
|
||||
|
@ -11,7 +10,7 @@ mkCoqDerivation {
|
|||
releaseRev = v: "mathcomp-odd-order.${v}";
|
||||
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch mathcomp.character.version [
|
||||
defaultVersion = with lib.versions; lib.switch mathcomp.character.version [
|
||||
{ case = (range "1.13.0" "1.15.0"); out = "1.14.0"; }
|
||||
{ case = (range "1.12.0" "1.14.0"); out = "1.13.0"; }
|
||||
{ case = (range "1.10.0" "1.12.0"); out = "1.12.0"; }
|
||||
|
@ -27,7 +26,7 @@ mkCoqDerivation {
|
|||
mathcomp.all
|
||||
];
|
||||
|
||||
meta = {
|
||||
meta = with lib; {
|
||||
description = "Formal proof of the Odd Order Theorem";
|
||||
maintainers = with maintainers; [ siraben ];
|
||||
license = licenses.cecill-b;
|
||||
|
|
|
@ -1,10 +1,10 @@
|
|||
{ lib, mkCoqDerivation, coq, version ? null }:
|
||||
|
||||
with lib; mkCoqDerivation {
|
||||
mkCoqDerivation {
|
||||
pname = "paco";
|
||||
owner = "snu-sf";
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch coq.coq-version [
|
||||
defaultVersion = with lib.versions; lib.switch coq.coq-version [
|
||||
{ case = range "8.12" "8.16"; out = "4.1.2"; }
|
||||
{ case = range "8.9" "8.13"; out = "4.1.1"; }
|
||||
{ case = range "8.6" "8.13"; out = "4.0.2"; }
|
||||
|
@ -27,6 +27,6 @@ with lib; mkCoqDerivation {
|
|||
meta = {
|
||||
homepage = "https://plv.mpi-sws.org/paco/";
|
||||
description = "A Coq library implementing parameterized coinduction";
|
||||
maintainers = with maintainers; [ jwiegley ptival ];
|
||||
maintainers = with lib.maintainers; [ jwiegley ptival ];
|
||||
};
|
||||
}
|
||||
|
|
|
@ -1,9 +1,9 @@
|
|||
{ lib, mkCoqDerivation, coq, version ? null }:
|
||||
|
||||
with lib; mkCoqDerivation {
|
||||
mkCoqDerivation {
|
||||
pname = "paramcoq";
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch coq.version [
|
||||
defaultVersion = with lib.versions; lib.switch coq.version [
|
||||
{ case = range "8.10" "8.16"; out = "1.1.3+coq${coq.coq-version}"; }
|
||||
{ case = range "8.7" "8.13"; out = "1.1.2+coq${coq.coq-version}"; }
|
||||
] null;
|
||||
|
@ -24,7 +24,7 @@ with lib; mkCoqDerivation {
|
|||
release."1.1.2+coq8.7".sha256 = "09n0ky7ldb24by7yf5j3hv410h85x50ksilf7qacl7xglj4gy5hj";
|
||||
releaseRev = v: "v${v}";
|
||||
mlPlugin = true;
|
||||
meta = {
|
||||
meta = with lib; {
|
||||
description = "Coq plugin for parametricity";
|
||||
license = licenses.mit;
|
||||
maintainers = [ maintainers.vbgl ];
|
||||
|
|
|
@ -1,6 +1,5 @@
|
|||
{ lib, mkCoqDerivation, coq, ceres, coq-ext-lib, version ? null }:
|
||||
|
||||
with lib;
|
||||
mkCoqDerivation {
|
||||
|
||||
pname = "parsec";
|
||||
|
@ -11,14 +10,14 @@ mkCoqDerivation {
|
|||
releaseRev = (v: "v${v}");
|
||||
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch coq.version [
|
||||
defaultVersion = with lib.versions; lib.switch coq.version [
|
||||
{ case = range "8.12" "8.16"; out = "0.1.1"; }
|
||||
{ case = range "8.12" "8.13"; out = "0.1.0"; }
|
||||
] null;
|
||||
release."0.1.1".sha256 = "sha256:1c0l18s68pzd4c8i3jimh2yz0pqm4g38pca4bm7fr18r8xmqf189";
|
||||
release."0.1.0".sha256 = "sha256:01avfcqirz2b9wjzi9iywbhz9szybpnnj3672dgkfsimyg9jgnsr";
|
||||
|
||||
meta = {
|
||||
meta = with lib; {
|
||||
description = "Library for serialization to S-expressions";
|
||||
license = licenses.bsd3;
|
||||
maintainers = with maintainers; [ Zimmi48 ];
|
||||
|
|
|
@ -1,5 +1,4 @@
|
|||
{ lib, mkCoqDerivation, coq, version ? null }:
|
||||
with lib;
|
||||
|
||||
mkCoqDerivation {
|
||||
pname = "pocklington";
|
||||
|
@ -9,11 +8,11 @@ mkCoqDerivation {
|
|||
release."8.12.0".sha256 = "sha256-0xBrw9+4g14niYdNqp0nx00fPJoSSnaDSDEaIVpPfjs=";
|
||||
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch coq.coq-version [
|
||||
defaultVersion = with lib.versions; lib.switch coq.coq-version [
|
||||
{ case = isGe "8.7"; out = "8.12.0"; }
|
||||
] null;
|
||||
|
||||
meta = {
|
||||
meta = with lib; {
|
||||
description = "Pocklington's criterion for primality in Coq";
|
||||
maintainers = with maintainers; [ siraben ];
|
||||
license = licenses.mit;
|
||||
|
|
|
@ -1,5 +1,4 @@
|
|||
{ lib, mkCoqDerivation, coq, ssreflect, version ? null }:
|
||||
with lib;
|
||||
|
||||
mkCoqDerivation {
|
||||
pname = "reglang";
|
||||
|
@ -9,14 +8,14 @@ mkCoqDerivation {
|
|||
release."1.1.2".sha256 = "sha256-SEnMilLNxh6a3oiDNGLaBr8quQ/nO2T9Fwdf/1il2Yk=";
|
||||
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch coq.coq-version [
|
||||
defaultVersion = with lib.versions; lib.switch coq.coq-version [
|
||||
{ case = range "8.10" "8.16"; out = "1.1.2"; }
|
||||
] null;
|
||||
|
||||
|
||||
propagatedBuildInputs = [ ssreflect ];
|
||||
|
||||
meta = {
|
||||
meta = with lib; {
|
||||
description = "Regular Language Representations in Coq";
|
||||
maintainers = with maintainers; [ siraben ];
|
||||
license = licenses.cecill-b;
|
||||
|
|
|
@ -1,12 +1,11 @@
|
|||
{ lib, mkCoqDerivation, coq, aac-tactics, mathcomp, version ? null }:
|
||||
with lib;
|
||||
|
||||
mkCoqDerivation {
|
||||
pname = "relation-algebra";
|
||||
owner = "damien-pous";
|
||||
|
||||
releaseRev = v:
|
||||
if versions.isGe "1.7.6" v
|
||||
if lib.versions.isGe "1.7.6" v
|
||||
then "v.${v}"
|
||||
else "v${v}";
|
||||
|
||||
|
@ -20,7 +19,7 @@ mkCoqDerivation {
|
|||
release."1.7.1".sha256 = "sha256-WWVMcR6z8rT4wzZPb8SlaVWGe7NC8gScPqawd7bltQA=";
|
||||
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch coq.coq-version [
|
||||
defaultVersion = with lib.versions; lib.switch coq.coq-version [
|
||||
{ case = isEq "8.16"; out = "1.7.8"; }
|
||||
{ case = isEq "8.15"; out = "1.7.7"; }
|
||||
{ case = isEq "8.14"; out = "1.7.6"; }
|
||||
|
@ -35,7 +34,7 @@ mkCoqDerivation {
|
|||
|
||||
propagatedBuildInputs = [ aac-tactics mathcomp.ssreflect ];
|
||||
|
||||
meta = {
|
||||
meta = with lib; {
|
||||
description = "Relation algebra library for Coq";
|
||||
maintainers = with maintainers; [ siraben ];
|
||||
license = licenses.gpl3Plus;
|
||||
|
|
|
@ -1,5 +1,4 @@
|
|||
{ lib, mkCoqDerivation, coq, version ? null }:
|
||||
with lib;
|
||||
|
||||
mkCoqDerivation rec {
|
||||
pname = "semantics";
|
||||
|
@ -15,7 +14,7 @@ mkCoqDerivation rec {
|
|||
release."8.6.0".sha256 = "sha256-GltkGQ3tJqUPAbdDkqqvKLLhMOap50XvGaCkjshiNdY=";
|
||||
|
||||
inherit version;
|
||||
defaultVersion = with versions; switch coq.coq-version [
|
||||
defaultVersion = with lib.versions; lib.switch coq.coq-version [
|
||||
{ case = range "8.10" "8.16"; out = "8.14.0"; }
|
||||
{ case = "8.9"; out = "8.9.0"; }
|
||||
{ case = "8.8"; out = "8.8.0"; }
|
||||
|
@ -34,7 +33,7 @@ mkCoqDerivation rec {
|
|||
done
|
||||
'';
|
||||
|
||||
meta = {
|
||||
meta = with lib; {
|
||||
description = "A survey of programming language semantics styles in Coq";
|
||||
longDescription = ''
|
||||
A survey of semantics styles in Coq, from natural semantics through
|
||||
|
|
|
@ -17,7 +17,7 @@ in
|
|||
inherit version release;
|
||||
|
||||
defaultVersion = with versions;
|
||||
switch coq.version [
|
||||
lib.switch coq.version [
|
||||
{ case = isEq "8.16"; out = "8.16.0+0.16.0"; }
|
||||
{ case = isEq "8.15"; out = "8.15.0+0.15.0"; }
|
||||
{ case = isEq "8.14"; out = "8.14.0+0.14.0"; }
|
||||
|
|
Some files were not shown because too many files have changed in this diff Show more
Loading…
Reference in a new issue