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.

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

coqPackages.trakt: init at 1.0, coqPackages.smtcoq: init at itp22 #162265

Merged
merged 3 commits into from Apr 15, 2022

Conversation

siraben
Copy link
Member

@siraben siraben commented Feb 28, 2022

Motivation for this change
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/)
  • 22.05 Release Notes (or backporting 21.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.

@siraben siraben force-pushed the smtcoq-init branch 2 times, most recently from aeb3444 to 0ee4a67 Compare February 28, 2022 21:39
@siraben
Copy link
Member Author

siraben commented Feb 28, 2022

Result of nixpkgs-review pr 162265 run on aarch64-darwin 1

2 packages built:
  • coqPackages.smtcoq
  • coqPackages.trakt

@auroraanna
Copy link
Contributor

Okay it doesn't work now. But I know why. I shouldn't have recommend the https:// protocol in this case because that repo is only available via git://. I didn't check that. Some I read that he git protocol is unsafe. Now I read up on git:// some more and the lack of authentication means that by default anyone can write to the repo. Fortunately the owners seem to have disabled that (I can't push to it) so it shouldn't be a problem. Sorry for the mess!

@siraben siraben changed the title coqPackages.trakt: init at 1.0 coqPackages.trakt: init at 1.0, coqPackages.smtcoq: init at itp22 Apr 15, 2022
@siraben
Copy link
Member Author

siraben commented Apr 15, 2022

Result of nixpkgs-review pr 162265 run on aarch64-darwin 1

3 packages marked as broken and skipped:
  • echidna
  • maude
  • tamarin-prover
1 package failed to build:
  • ginac
4 packages built:
  • cln
  • coqPackages.smtcoq
  • coqPackages.trakt
  • cvc4

@siraben siraben merged commit 7c188d8 into NixOS:master Apr 15, 2022
@siraben siraben deleted the smtcoq-init branch April 15, 2022 14:44
@CohenCyril
Copy link
Contributor

nix-build -A cvc4
these derivations will be built:
  /nix/store/s12fa4gvhv4nkll56nmhjm2dbm5v03y8-cln-1.3.6.drv
  /nix/store/lg77x1k703m73xdizw40nblmgyny57ic-cvc4-1.8.drv
these paths will be fetched (82.92 MiB download, 199.37 MiB unpacked):
  /nix/store/7hl64m5n08z8hqclm2mvqj4ka4i32q47-gnome-vfs-2.24.4
  /nix/store/ahl8r4p0cnqwrqapp5546gd7idz4vrhg-openjdk-8u322-ga
  /nix/store/bdxvdpcn56qam3wv0pm1nb39747a7dli-openjdk-8u322-ga-jre
  /nix/store/ixsi2hwc2w5awxkhjxqk4fr5lfa725v2-antlr-3.4
copying path '/nix/store/7hl64m5n08z8hqclm2mvqj4ka4i32q47-gnome-vfs-2.24.4' from 'https://cache.nixos.org'...
building '/nix/store/s12fa4gvhv4nkll56nmhjm2dbm5v03y8-cln-1.3.6.drv'...
unpacking sources
unpacking source archive /nix/store/3jzdpn5lg48dkm6ci6zyg0s8vfkd5r3h-cln
source root is cln
patching sources
configuring
no configure script, doing nothing
building
no Makefile, doing nothing
installing
install flags: SHELL=/nix/store/30j23057fqnnc1p4jqmq73p0gxgn0frq-bash-5.1-p16/bin/bash install
make: *** No rule to make target 'install'.  Stop.
builder for '/nix/store/s12fa4gvhv4nkll56nmhjm2dbm5v03y8-cln-1.3.6.drv' failed with exit code 2
cannot build derivation '/nix/store/lg77x1k703m73xdizw40nblmgyny57ic-cvc4-1.8.drv': 1 dependencies couldn't be built
error: build of '/nix/store/lg77x1k703m73xdizw40nblmgyny57ic-cvc4-1.8.drv' failed

@siraben
Copy link
Member Author

siraben commented Apr 15, 2022

@CohenCyril what system does this build log correspond to?

@CohenCyril
Copy link
Contributor

NixOS x86_64

@CohenCyril
Copy link
Contributor

On the master branch of nixpkgs

@siraben
Copy link
Member Author

siraben commented Apr 15, 2022

For some reason my patch works on darwin but causes linux to fail. Build error on darwin with the previous definition of cln: http://ix.io/3VeA

@hqurve
Copy link
Contributor

hqurve commented Apr 15, 2022

After a bit of testing, it appears as if fetchGit is not working correctly with this site. By inspecting the src by running nix build .#cln.src, the directory structure is much more similar to the master branch than it is to the 1.3.6 release. Notice that the CMakeList.txt file is not present on 1.3.6.

I also tried supplying the commit hash, but to no avail

@gebner
Copy link
Member

gebner commented Apr 17, 2022

I'm really surprised that ofborg didn't fail CI here even though cln failed to build: https://logs.nix.ci/?key=nixos/nixpkgs.162265&attempt_id=b7315ae6-ac87-448d-a6b4-4bfc712ab818

error: build of '/nix/store/dqninbrx9wp5rln6amikn5w76xxr1lkl-coq8.13-smtcoq-itp22.drv', '/nix/store/s12fa4gvhv4nkll56nmhjm2dbm5v03y8-cln-1.3.6.drv' failed

@CohenCyril
Copy link
Contributor

CohenCyril commented May 3, 2022

@siraben I didn't manage to compile smtcoq for coq 8.14 and 8.15 and is documented as such in the release .opam file. Did you ever test it for Coq 8.14 and 8.15?

@siraben siraben mentioned this pull request May 13, 2022
13 tasks
siraben added a commit to siraben/nixpkgs that referenced this pull request May 13, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

5 participants