cedille: init at v1.0.0 #48288

mpickering · 2018-10-12T21:30:15Z

Motivation for this change

Things done

Tested using sandboxing (nix.useSandbox on NixOS, or option sandbox in nix.conf on non-NixOS)
Built on platform(s)
- NixOS
- macOS
- other Linux distributions
Tested via one or more NixOS test(s) if existing and applicable for the change (look inside nixos/tests)
Tested compilation of all pkgs that depend on this change using nix-shell -p nox --run "nox-review wip"
Tested execution of all binary files (usually in ./result/bin/)
Determined the impact on package closure size (by running nix path-info -S before and after)
Fits CONTRIBUTING.md.

mpickering · 2018-10-12T21:46:28Z

I should also probably package the elisp code but that can be a separate PR I think? I need to check what agda does.

mpickering · 2018-10-13T17:07:54Z

I packaged the elisp now as well.

Here's an example of how to set up emacs to use this modes.

https://gist.github.com/0971d372954137c4578ae9c06d31414c

let
  np = import <nixpkgs> {};
  myEmacsConfig = np.writeText "default.el" ''
;; initialize package
(require 'package)
(package-initialize 'noactivate)
;; load some packages
(setq cedille-path "${np.cedille}/bin")
(require 'cedille-mode)
    '';
    myEmacs = np.emacsWithPackages (epkgs: (with epkgs; [
      (np.runCommand "default.el" {} ''
mkdir -p $out/share/emacs/site-lisp
cp ${myEmacsConfig} $out/share/emacs/site-lisp/default.el
'')
      np.emacsPackages.cedille
      melpaStablePackages.use-package
    ]));
in
  np.mkShell { buildInputs = [ myEmacs ];}

infinisil

Would be nice to have the emacs mode patched so that it finds the cedille binary by default, see https://github.com/cedille/cedille/blob/0cac62eef32b49af77c475f1b3f4d271f83a0b4b/cedille-mode.el#L32

Also, eval error needs to be fixed, not sure what's up with that

infinisil · 2018-10-14T15:12:39Z

pkgs/applications/science/logic/cedille/default.nix

+{ stdenv, fetchFromGitHub, alex, happy, Agda, agdaIowaStdlib,
+  glibcLocales, ghcWithPackages }:
+let
+in


empty let in

mpickering · 2018-10-14T17:13:40Z

I have no idea why CI fails.

infinisil · 2018-10-14T17:24:30Z

pkgs/applications/editors/emacs-modes/cedille/default.nix

+    install cedille-mode/*.el cedille-mode/*.elc $out/share/emacs/site-lisp
+    install *.el *.elc $out/share/emacs/site-lisp
+    substitute $out/share/emacs/site-lisp/cedille-mode.el $out/share/emacs/site-lisp/cedille-mode.el \
+      --replace /usr/bin/cedille ${cedille}/bin/cedille \


There's substituteInPlace for this too

GrahamcOfBorg · 2018-10-14T17:57:15Z

Unexpected error: command failed with exit code 1 on x86_64-darwin (full log)

Attempted: cedille

Partial log (click to expand)

copying path '/nix/store/sxmgwq3dj5lfxifjsynz62hr9bxw4hzz-Agda-2.5.4.1' from 'https://cache.nixos.org'...

trying https://github.com/cedille/ial/archive/v1.4.0.tar.gz
  % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
                                 Dload  Upload   Total   Spent    Left  Speed
100   119    0   119    0     0    252      0 --:--:-- --:--:-- --:--:--   251
100 57443    0 57443    0     0  48312      0 --:--:--  0:00:01 --:--:-- 3015k
unpacking source archive /private/tmp/nix-build-source.drv-1/v1.4.0.tar.gz
cannot build derivation '/nix/store/d2f78hp4z3ydysyhgpqg46iw5g88nbgx-cedille-1.0.0.drv': 1 dependencies couldn't be built
error: build of '/nix/store/d2f78hp4z3ydysyhgpqg46iw5g88nbgx-cedille-1.0.0.drv' failed

GrahamcOfBorg · 2018-10-14T18:01:25Z

Success on x86_64-linux (full log)

Attempted: cedille

Partial log (click to expand)

mv src/main cedille
installing
post-installation fixup
shrinking RPATHs of ELF executables and libraries in /nix/store/hhbys81xvj0fsxz4gi4v8kf09mq06cp4-cedille-1.0.0
shrinking /nix/store/hhbys81xvj0fsxz4gi4v8kf09mq06cp4-cedille-1.0.0/bin/cedille
strip is /nix/store/vcc4svb8gy29g4pam2zja6llkbcwsyiq-binutils-2.30/bin/strip
stripping (with command strip and flags -S) in /nix/store/hhbys81xvj0fsxz4gi4v8kf09mq06cp4-cedille-1.0.0/bin
patching script interpreter paths in /nix/store/hhbys81xvj0fsxz4gi4v8kf09mq06cp4-cedille-1.0.0
checking for references to /build in /nix/store/hhbys81xvj0fsxz4gi4v8kf09mq06cp4-cedille-1.0.0...
/nix/store/hhbys81xvj0fsxz4gi4v8kf09mq06cp4-cedille-1.0.0

mpickering · 2018-10-14T18:12:55Z

Should be good to merge now.

infinisil · 2018-10-14T18:15:48Z

Why the hash mismatch on Darwin though?

GrahamcOfBorg · 2018-10-14T18:56:33Z

Timed out, unknown build status on aarch64-linux (full log)

Attempted: cedille

Partial log (click to expand)

cannot build derivation '/nix/store/529sabir90d9s37qhm8pfdnqmchl5q3d-unordered-containers-0.2.9.0.drv': 9 dependencies couldn't be built
cannot build derivation '/nix/store/mvyh0yjafc7zjc23clyx8ad3s6r2qywk-tasty-1.1.0.3.drv': 9 dependencies couldn't be built
cannot build derivation '/nix/store/cwbn2i2n3pdp96mpscdakxgn0fv3frxv-uri-encode-1.5.0.5.drv': 4 dependencies couldn't be built
cannot build derivation '/nix/store/gi91g8hngmma5lri66gciqz9r73wfp9i-tasty-hunit-0.10.0.1.drv': 4 dependencies couldn't be built
cannot build derivation '/nix/store/cvmlb04njlzy6vbx1wf3dll0shjp97fq-tasty-quickcheck-0.10.drv': 9 dependencies couldn't be built
cannot build derivation '/nix/store/i23wf2yjnil909myxa651grc4wwa0194-blaze-markup-0.8.2.2.drv': 9 dependencies couldn't be built
cannot build derivation '/nix/store/l86hjyxf6zngsr8nv7cfdcd316ib8mdm-blaze-html-0.9.1.1.drv': 10 dependencies couldn't be built
cannot build derivation '/nix/store/pvzymxfsckb6i7rkhx5w1zyawcncj64d-Agda-2.5.4.1.drv': 24 dependencies couldn't be built
cannot build derivation '/nix/store/drc00psxyr5a0q2nky7zzx6zi4v5ysap-cedille-1.0.0.drv': 4 dependencies couldn't be built
error: build of '/nix/store/drc00psxyr5a0q2nky7zzx6zi4v5ysap-cedille-1.0.0.drv' failed

mpickering · 2018-10-14T18:57:26Z

I don't know but it's a standard use of fetchFromGitHub.

infinisil · 2018-10-14T19:00:54Z

Let's just try again, maybe it'll work now

@GrahamcOfBorg build cedille

GrahamcOfBorg · 2018-10-14T19:01:26Z

Unexpected error: command failed with exit code 1 on x86_64-darwin (full log)

Attempted: cedille

Partial log (click to expand)


trying https://github.com/cedille/cedille/archive/v1.0.0.tar.gz
  % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
                                 Dload  Upload   Total   Spent    Left  Speed
100   123    0   123    0     0    247      0 --:--:-- --:--:-- --:--:--   247
100 1892k    0 1892k    0     0  1074k      0 --:--:--  0:00:01 --:--:-- 3724k
unpacking source archive /private/tmp/nix-build-source.drv-0/v1.0.0.tar.gz
fixed-output derivation produced path '/nix/store/3zp53g8817gc224ydbwjd1xy26cs771n-source' with sha256 hash '0csbi1mp72na5j5ymy2fhkn6bcyxp443dxwl1aphcq4inwy0r95g' instead of the expected hash '08c2vgg8i6l3ws7hd5gsj89mki36lxm7x7s8hi1qa5gllq04a832'
cannot build derivation '/nix/store/d2f78hp4z3ydysyhgpqg46iw5g88nbgx-cedille-1.0.0.drv': 1 dependencies couldn't be built
error: build of '/nix/store/d2f78hp4z3ydysyhgpqg46iw5g88nbgx-cedille-1.0.0.drv' failed

GrahamcOfBorg · 2018-10-14T19:01:47Z

Success on x86_64-linux (full log)

Attempted: cedille

Partial log (click to expand)

/nix/store/hhbys81xvj0fsxz4gi4v8kf09mq06cp4-cedille-1.0.0

infinisil

@LnL7 mentioned in #nixos-borg that it might be unicode normalization on macOS, see also #48128 (comment)

Seems fine to me then :)

infinisil · 2018-10-14T19:14:11Z

Oh actually, one last thing: The commits are named a bit unconventional. First one should be agdaIowaStdlib: 18734 -> 1.4.0, second should be cedille: init at 1.0.0, third should be emacsPackages.cedille: init at 1.0.0

mpickering · 2018-10-14T19:20:43Z

Done.

GrahamcOfBorg · 2018-10-14T19:34:18Z

Unexpected error: command failed with exit code 1 on x86_64-darwin (full log)

Attempted: agdaIowaStdlib, cedille

Partial log (click to expand)

agda  -v 0 sum-thms.agda
agda  -v 0 tree-test.agda
agda  -v 0 trie-thms.agda
agda  -v 0 vector-test.agda
agda  -v 0 vector-sort.agda
installing
post-installation fixup
strip is /nix/store/53nysl8bqwxihwzs1pgwka20nf8mbvlp-cctools-binutils-darwin/bin/strip
patching script interpreter paths in /nix/store/fv8y6qwxywlljnca4yq8p490drl6shr0-agda-iowa-stdlib-1.4.0
error: build of '/nix/store/d2f78hp4z3ydysyhgpqg46iw5g88nbgx-cedille-1.0.0.drv' failed

GrahamcOfBorg · 2018-10-14T19:34:37Z

Success on x86_64-linux (full log)

Attempted: agdaIowaStdlib, cedille

Partial log (click to expand)

agda  -v 0 vector-test.agda
agda  -v 0 vector-sort.agda
installing
post-installation fixup
shrinking RPATHs of ELF executables and libraries in /nix/store/x4grq4nk1z3p49zlnbqhy3yqdmaai9bb-agda-iowa-stdlib-1.4.0
strip is /nix/store/vcc4svb8gy29g4pam2zja6llkbcwsyiq-binutils-2.30/bin/strip
patching script interpreter paths in /nix/store/x4grq4nk1z3p49zlnbqhy3yqdmaai9bb-agda-iowa-stdlib-1.4.0
checking for references to /build in /nix/store/x4grq4nk1z3p49zlnbqhy3yqdmaai9bb-agda-iowa-stdlib-1.4.0...
/nix/store/x4grq4nk1z3p49zlnbqhy3yqdmaai9bb-agda-iowa-stdlib-1.4.0
/nix/store/hhbys81xvj0fsxz4gi4v8kf09mq06cp4-cedille-1.0.0

GrahamcOfBorg · 2018-10-14T20:01:16Z

Timed out, unknown build status on aarch64-linux (full log)

Attempted: cedille

Partial log (click to expand)

cannot build derivation '/nix/store/529sabir90d9s37qhm8pfdnqmchl5q3d-unordered-containers-0.2.9.0.drv': 9 dependencies couldn't be built
cannot build derivation '/nix/store/mvyh0yjafc7zjc23clyx8ad3s6r2qywk-tasty-1.1.0.3.drv': 9 dependencies couldn't be built
cannot build derivation '/nix/store/cwbn2i2n3pdp96mpscdakxgn0fv3frxv-uri-encode-1.5.0.5.drv': 4 dependencies couldn't be built
cannot build derivation '/nix/store/gi91g8hngmma5lri66gciqz9r73wfp9i-tasty-hunit-0.10.0.1.drv': 4 dependencies couldn't be built
cannot build derivation '/nix/store/cvmlb04njlzy6vbx1wf3dll0shjp97fq-tasty-quickcheck-0.10.drv': 9 dependencies couldn't be built
cannot build derivation '/nix/store/i23wf2yjnil909myxa651grc4wwa0194-blaze-markup-0.8.2.2.drv': 9 dependencies couldn't be built
cannot build derivation '/nix/store/l86hjyxf6zngsr8nv7cfdcd316ib8mdm-blaze-html-0.9.1.1.drv': 10 dependencies couldn't be built
cannot build derivation '/nix/store/pvzymxfsckb6i7rkhx5w1zyawcncj64d-Agda-2.5.4.1.drv': 24 dependencies couldn't be built
cannot build derivation '/nix/store/drc00psxyr5a0q2nky7zzx6zi4v5ysap-cedille-1.0.0.drv': 4 dependencies couldn't be built
error: build of '/nix/store/drc00psxyr5a0q2nky7zzx6zi4v5ysap-cedille-1.0.0.drv' failed

GrahamcOfBorg · 2018-10-14T21:01:22Z

Timed out, unknown build status on aarch64-linux (full log)

Attempted: agdaIowaStdlib, cedille

Partial log (click to expand)

cannot build derivation '/nix/store/mvyh0yjafc7zjc23clyx8ad3s6r2qywk-tasty-1.1.0.3.drv': 9 dependencies couldn't be built
cannot build derivation '/nix/store/cwbn2i2n3pdp96mpscdakxgn0fv3frxv-uri-encode-1.5.0.5.drv': 4 dependencies couldn't be built
cannot build derivation '/nix/store/gi91g8hngmma5lri66gciqz9r73wfp9i-tasty-hunit-0.10.0.1.drv': 4 dependencies couldn't be built
cannot build derivation '/nix/store/cvmlb04njlzy6vbx1wf3dll0shjp97fq-tasty-quickcheck-0.10.drv': 9 dependencies couldn't be built
cannot build derivation '/nix/store/i23wf2yjnil909myxa651grc4wwa0194-blaze-markup-0.8.2.2.drv': 9 dependencies couldn't be built
cannot build derivation '/nix/store/l86hjyxf6zngsr8nv7cfdcd316ib8mdm-blaze-html-0.9.1.1.drv': 10 dependencies couldn't be built
cannot build derivation '/nix/store/pvzymxfsckb6i7rkhx5w1zyawcncj64d-Agda-2.5.4.1.drv': 24 dependencies couldn't be built
cannot build derivation '/nix/store/fnxapyxihdfp03a91h0npyy9hs8rirs6-agda-iowa-stdlib-1.4.0.drv': 1 dependencies couldn't be built
cannot build derivation '/nix/store/drc00psxyr5a0q2nky7zzx6zi4v5ysap-cedille-1.0.0.drv': 4 dependencies couldn't be built
error: build of '/nix/store/drc00psxyr5a0q2nky7zzx6zi4v5ysap-cedille-1.0.0.drv', '/nix/store/fnxapyxihdfp03a91h0npyy9hs8rirs6-agda-iowa-stdlib-1.4.0.drv' failed

adisbladis · 2020-05-16T09:53:25Z

@mpickering The cedille build is failing both on unstable and 20.03.

mpickering · 2020-05-16T09:55:44Z

@adisbladis Perhaps something which should be fixed by #76653 ? I have not used this package since I packaged it.

adisbladis · 2020-05-16T11:45:55Z

@mpickering Nope, it's not fixed by #76653.

GrahamcOfBorg added the 6.topic: emacs label Oct 13, 2018

infinisil requested changes Oct 14, 2018

View reviewed changes

mpickering force-pushed the cedille branch from 547eef6 to 52cfe9f Compare October 14, 2018 17:06

infinisil reviewed Oct 14, 2018

View reviewed changes

mpickering force-pushed the cedille branch from 52cfe9f to d7b883d Compare October 14, 2018 17:43

GrahamcOfBorg added 8.has: package (new) 10.rebuild-darwin: 1-10 10.rebuild-linux: 1-10 labels Oct 14, 2018

infinisil approved these changes Oct 14, 2018

View reviewed changes

mpickering added 3 commits October 14, 2018 19:17

agdaIowaStdlib: 18734 -> 1.4.0

561fcf4

cedille: init at 1.0.0

43ae337

emacsPackages.cedille: init at 1.0.0

9e348b4

mpickering force-pushed the cedille branch from d7b883d to 9e348b4 Compare October 14, 2018 19:18

infinisil merged commit 2551412 into NixOS:master Oct 14, 2018

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

cedille: init at v1.0.0 #48288

cedille: init at v1.0.0 #48288

mpickering commented Oct 12, 2018

mpickering commented Oct 12, 2018

mpickering commented Oct 13, 2018

infinisil left a comment

infinisil Oct 14, 2018

mpickering commented Oct 14, 2018

infinisil Oct 14, 2018

GrahamcOfBorg commented Oct 14, 2018

GrahamcOfBorg commented Oct 14, 2018

mpickering commented Oct 14, 2018

infinisil commented Oct 14, 2018

GrahamcOfBorg commented Oct 14, 2018

mpickering commented Oct 14, 2018

infinisil commented Oct 14, 2018

GrahamcOfBorg commented Oct 14, 2018

GrahamcOfBorg commented Oct 14, 2018

infinisil left a comment

infinisil commented Oct 14, 2018 •

edited

mpickering commented Oct 14, 2018

GrahamcOfBorg commented Oct 14, 2018

GrahamcOfBorg commented Oct 14, 2018

GrahamcOfBorg commented Oct 14, 2018

GrahamcOfBorg commented Oct 14, 2018

adisbladis commented May 16, 2020

mpickering commented May 16, 2020

adisbladis commented May 16, 2020

cedille: init at v1.0.0 #48288

cedille: init at v1.0.0 #48288

Conversation

mpickering commented Oct 12, 2018

Motivation for this change

Things done

mpickering commented Oct 12, 2018

mpickering commented Oct 13, 2018

infinisil left a comment

Choose a reason for hiding this comment

infinisil Oct 14, 2018

Choose a reason for hiding this comment

mpickering commented Oct 14, 2018

infinisil Oct 14, 2018

Choose a reason for hiding this comment

GrahamcOfBorg commented Oct 14, 2018

GrahamcOfBorg commented Oct 14, 2018

mpickering commented Oct 14, 2018

infinisil commented Oct 14, 2018

GrahamcOfBorg commented Oct 14, 2018

mpickering commented Oct 14, 2018

infinisil commented Oct 14, 2018

GrahamcOfBorg commented Oct 14, 2018

GrahamcOfBorg commented Oct 14, 2018

infinisil left a comment

Choose a reason for hiding this comment

infinisil commented Oct 14, 2018 • edited

mpickering commented Oct 14, 2018

GrahamcOfBorg commented Oct 14, 2018

GrahamcOfBorg commented Oct 14, 2018

GrahamcOfBorg commented Oct 14, 2018

GrahamcOfBorg commented Oct 14, 2018

adisbladis commented May 16, 2020

mpickering commented May 16, 2020

adisbladis commented May 16, 2020

infinisil commented Oct 14, 2018 •

edited