cornelis: init at 2024-04-08

[phijor]

Description of changes

This PR adds a package containing the binary of Cornelis, which provides editor-integration for Agda in Neovim.

This is a Haskell package, but it is not available on hackage. It therefore includes an update-script to generate the derivation with cabal2nix.

The upstream repository includes a Neovim plugin which should be packaged in a future PR. I personally do not configure Neovim through Nix, so any help with that would be appreciated.

Edit: I packaged a first iteration of the vim plugin.

Things done

• Built on platform(s)
  • x86_64-linux
  • aarch64-linux
  • x86_64-darwin
  • aarch64-darwin
• For non-Linux: Is sandboxing enabled in nix.conf? (See Nix manual)
  • sandbox = relaxed
  • sandbox = true
• Tested, as applicable:
  • NixOS test(s) (look inside nixos/tests)
  • and/or package tests
  • or, for functions and "core" functionality, tests in lib/tests or pkgs/test
  • made sure NixOS tests are linked to the relevant packages
• Tested compilation of all packages that depend on this change using nix-shell -p nixpkgs-review --run "nixpkgs-review rev HEAD". Note: all changes have to be committed, also see nixpkgs-review usage
• Tested basic functionality of all binary files (usually in ./result/bin/)
• 24.05 Release Notes (or backporting 23.05 and 23.11 Release notes)
  • (Package updates) Added a release notes entry if the change is major or breaking
  • (Module updates) Added a release notes entry if the change is significant
  • (Module addition) Added a release notes entry if adding a new NixOS module
• Fits CONTRIBUTING.md.

---

Add a 👍 reaction to pull requests you find important.

[phijor]

@malob, I have seen your contributions to the upstream Nix flake. Would you have the capacity to co-maintain the package here?

[phijor]

Result of nixpkgs-review pr 304335 run on x86_64-linux 1

1 package built:

• cornelis

[phijor]

I've been reading some other PRs adding Haskell packages and have learned that non-hackage-packages.nix is a thing. I'll try to add the package there instead.

cc @sternenseemann is there documentation on how to add non-hackage packages?

[malob]

I think your derivation can be a lot simpler. This worked for me:

{ haskellPackages, fetchFromGitHub }:

let
  pname = "cornelis";
  src = fetchFromGitHub {
    owner = "isovector";
    repo = pname;
    rev = "9d3347e7d8589a28bcdd283001367d60bacf6b05";
    hash = "sha256-KaAhKeESwOQ0R0vxeAO/CDPiPimiemoARyr0uIVTQ4w=";
  };
in

haskellPackages.callCabal2nix pname src {}

[malob]

If you're going to add cornelis to nixpkgs probably also worth adding the Vim plugin. Something like the following should do it in pkgs/applications/editors/vim/plugins/overrides.nix:

{ lib
[...]
, cornelis
[...]
,
}: self: super:
{
  [...]
  cornelis = buildVimPlugin {
    inherit (cornelis) pname version src;
    dependencies = with super; [ nvim-hs-vim vim-textobj-user ];
  };
  [...]
}

[malob]

Oh yeah, sure, you can list me as a co-maintainer.

[phijor]

I think your derivation can be a lot simpler. This worked for me:

I think your code performs an Import From Derivation, which is disallowed in nixpkgs. So running cabal2nix and committing the generated file is probably the way to go.

If you're going to add cornelis to nixpkgs probably also worth adding the Vim plugin. Something like the following should do it in pkgs/applications/editors/vim/plugins/overrides.nix:

Ahhh, that's a great suggestion, thank you. I believe in this case we should set g:cornelis_use_global_binary = 1 and point the plugin to the right binary. Let me figure out how to do that.

Oh yeah, sure, you can list me as a co-maintainer.

I'll do that!

[phijor]

Cornelis is now on Hackage. I guess we could wait for the next update to the Haskell package set here and then drop the custom packaging.

[malob]

I think waiting for haskellPackages update is probably the right call.

[phijor]

#307204 includes the package from hackage. Once that’s been merged into master, I’ll rebase and remove the custom packaging.

[phijor]

I rebased this on master after #307204 got merged. Of course the version of cornelis imported from Hackage is broken; 8be493a attempts to work around the problem (which has been reported at agda/cornelis#150).

465ae2d still includes some custom packaging for the top-level package: it sets some meta data and minimizes derivation size.

[ncfavier]

Looks good