Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

coqPackages_8_16.coq-lsp: init at 0.1.6+8.16 #213397

Merged
merged 2 commits into from Feb 25, 2023
Merged

coqPackages_8_16.coq-lsp: init at 0.1.6+8.16 #213397

merged 2 commits into from Feb 25, 2023

Conversation

marsam
Copy link
Contributor

@marsam marsam commented Jan 29, 2023

Description of changes

Add https://github.com/ejgallego/coq-lsp

Things done
  • Built on platform(s)
    • x86_64-linux
    • aarch64-linux
    • x86_64-darwin
    • aarch64-darwin
  • For non-Linux: Is sandbox = true set in nix.conf? (See Nix manual)
  • Tested, as applicable:
  • 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/)
  • 23.05 Release Notes (or backporting 22.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
    • (Release notes changes) Ran nixos/doc/manual/md-to-db.sh to update generated release notes
  • Fits CONTRIBUTING.md.

Thesola10
Thesola10 suggested changes Jan 31, 2023
View reviewed changes
pkgs/top-level/all-packages.nix Outdated Show resolved Hide resolved
@vbgl
Copy link
Contributor

vbgl commented Feb 1, 2023

It seems that version 0.1.4 is out, right?

@marsam
Copy link
Contributor Author

marsam commented Feb 1, 2023 •
edited

Thank you for reviewing. I moved the expression to coq-packages.nix and updated it to 0.1.4.
Tomorrow I will test if it's still working, I'm a bit busy with work.

Thesola10
Thesola10 approved these changes Feb 2, 2023
View reviewed changes
Copy link
Contributor

@Thesola10 Thesola10 left a comment •
edited

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM

pkgs/development/coq-modules/coq-lsp/default.nix Outdated
Comment on lines 11 to 15
inherit version;
defaultVersion = with lib.versions; lib.switch coq.coq-version [
{ case = range "8.16" "8.17"; out = "0.1.4+v8.16"; }
] null;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

this lsp won't work on Coq older than 8.16 I take it

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Folks thanks for this PR, for Coq 8.17 you need a 8.17 specific tree, unfortunately the Coq API we use is not stable between versions.

Tag for 8.17 is 0.1.4+v8.17

Copy link
Contributor

@Thesola10 Thesola10 Feb 7, 2023 •
edited

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Then it should be possible to use "0.1.4+v${coq.coq-version}", that's the beauty about a functional language

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It should yes! Something that has been brought to my attention is whether the branch names should be +v8.16 or +8.16, it seems the lastest scheme is the standard (including in some of my packages) so I'm unsure if I should tweak the tag names for the upcoming releases (and add the corresponding aliases back)

Any advice you folks have here as to easy packaging is most welcome.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It would be preferable, as I think the v messes up the reverse package name parser (e.g. when doing nix-env -e coq-lsp it tries to strip the version suffix)

Copy link

@ejgallego ejgallego Feb 7, 2023 •
edited

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks @Thesola10 , so to confirm 0.1.4+8.16 is more Nix-friendly than 0.1.4+v8.16?

Copy link
Contributor

@Thesola10 Thesola10 Feb 11, 2023 •
edited

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You might not need to change your actual tagging scheme -- since mkDerivation accepts arbitrary key/values, you could define a packageVersion = "0.1.4" and compose the derivation's version as "${packageVersion}+${coq.coq-version}" and the source tag as "${packageVersion}+v${coq.coq-version}"

@Thesola10 Thesola10 requested a review from vbgl February 3, 2023 10:54
vbgl
vbgl reviewed Feb 3, 2023
View reviewed changes
pkgs/top-level/coq-packages.nix Outdated Show resolved Hide resolved
pkgs/development/coq-modules/coq-lsp/default.nix Outdated Show resolved Hide resolved
@Alizter
Copy link
Contributor

Alizter commented Feb 15, 2023

Hi, coq-lsp 0.1.5 has been released. Would we be able to bump the version here?

@Alizter
Copy link
Contributor

Alizter commented Feb 15, 2023

Also we have a flake capable of building that has been merged, does that help things?

@ejgallego
Copy link

Hi @Alizter I'd suggest packaging 0.1.6 which is just out.

coq-lsp is a standard dune package (an vscode extension) so as long as Coq kinda works things should be fine, it also obeys COQLIB and COQPATH if Nix is using them.

@marsam
Copy link
Contributor Author

marsam commented Feb 22, 2023

Thank you for your reviews. I updated the expression to 0.1.6+8.16 and tested it works correctly.

@marsam marsam changed the title coq-lsp: init at 0.1.3+v8.16 coqPackages_8_16.coq-lsp: init at 0.1.6+8.16 Feb 22, 2023
@ofborg ofborg bot requested a review from Zimmi48 February 22, 2023 08:30
vbgl
vbgl approved these changes Feb 22, 2023
View reviewed changes
Copy link
Contributor

@vbgl vbgl left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I did not test, but it looks good.

@ejgallego
Copy link

Great @marsam , thank you very much!

We've detected a bug specific to 8.16 support (we usually test in 8.17), it is a small bug but annoying, we put a new https://github.com/ejgallego/coq-lsp/releases/tag/0.1.6.1%2B8.16 tag with the 8.16 specific fix.

@marsam
Copy link
Contributor Author

marsam commented Feb 22, 2023

Updated to 0.1.6.1+8.16

@marsam marsam merged commit 58f7e4a into NixOS:master Feb 25, 2023
@marsam marsam deleted the add-coq-lsp branch February 25, 2023 14:27
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ejgallego ejgallego ejgallego left review comments

@Thesola10 Thesola10 Thesola10 approved these changes

@vbgl vbgl vbgl approved these changes

@Zimmi48 Zimmi48 Awaiting requested review from Zimmi48

Assignees
No one assigned
Labels
8.has: package (new) 10.rebuild-darwin: 1-10 10.rebuild-linux: 1-10 11.by: package-maintainer 12.approvals: 1
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
6 participants
@marsam @vbgl @Alizter @ejgallego @Thesola10 @mweinelt