Stream: math-comp users

Topic: NIX CI testing with classical and analysis


view this post on Zulip Florent Hivert (Feb 01 2024 at 16:07):

I'm trying to adapt the CI with nix to my repo https://github.com/hivert/FormalPowerSeries. I've created a branch with a PR https://github.com/hivert/FormalPowerSeries/pull/3 (only the last few commit are relevant - It is based on the mathcomp2 branch with is not yet merged)...

The CI himself works, but I can't manage to properly set-up what is needed to use the classical reasoning. Specifically, If I don't require it, then the tests fails as expected with (after several early warning that boolp.v is missing):

Error: Cannot find a physical path bound to logical path
       > boolp with prefix mathcomp.

since classical reasoning is not installed. On the other hand, if I add it as

{ lib, mkCoqDerivation, which, coq
  , mathcomp-ssreflect, mathcomp-algebra, mathcomp-anaysis,
    multinomials, hierarchy-builder
  ## declare extra dependencies here, to be used in propagateBuildInputs e.g.
  # , mathcomp, coq-elpi
  , version ? null }:

and

  propagatedBuildInputs =
    [ mathcomp-ssreflect mathcomp-algebra mathcomp-analysis
      multinomials hierarchy-builder ];

Then CI fails much earlier at the stage

Checking presence of CI target fpseries
Run nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \
Error: Process completed with exit code 1.

with no clear error message. Without any diagnoses element, I'm not sure why. Is it because I required

 coqPackages.mathcomp.override.version = "2.2.0";

and there is no analysis at version 2.2.0 ? How can I fix this ? Thanks for any help !

view this post on Zulip Pierre Roux (Feb 01 2024 at 16:13):

I would say that you need to express the dependency to mathcomp-classical in the propagatedBuildInputs variable in .nix/coq-overlays/fpseries/default.nix

view this post on Zulip Florent Hivert (Feb 01 2024 at 16:18):

That's what I'm doing ! I forgot to precise that putting either 'mathcomp-analysis' or 'mathcomp-classical' leads to CI failing at the 'Checking presence of CI target fpseries' long before trying to compile.

view this post on Zulip Pierre Roux (Feb 01 2024 at 16:35):

You should try locally because unfortunately the CI is masking the output of nix-build ... --dry-run

view this post on Zulip Florent Hivert (Feb 01 2024 at 16:42):

I didn't know that running locally is feasible (I'm new to NIX, just trying to adapt some existing config).
The error is

error: Package coq8.17-mathcomp2.2-mathcomp-classical-broken in /nix/store/jvvz6rbi9mncjf9hh57pgafl20q0zvrg-source/pkgs/development/coq-modules/mathcomp-analysis/default.nix:67 is marked as broken, refusing to evaluate.

which confirm my diagnoses as far as I understand. Is that true ?

view this post on Zulip Cyril Cohen (Feb 01 2024 at 17:01):

I think your problem is simply that mathcomp classical and analysis 1.0.0 (i.e. the one compatible with mathcomp 2.x) where not released yet in nix. Cf https://coq.zulipchat.com/#narrow/stream/290990-Nix-toolbox-devs-.26-users/topic/mathcomp-analysis.20outdated.20in.20Nix.20repo

view this post on Zulip Florent Hivert (Feb 01 2024 at 17:05):

Did you just did it ? Or did the fact that I wrote

    coqPackages.mathcomp-classical.override.version = "1.0.0";

solve the problem using

 /nix/store/1bcyd7v30is0ii8h81drd92sxiycjzyr-coq8.19-mathcomp2.2-mathcomp-classical-dev

view this post on Zulip Pierre Roux (Feb 01 2024 at 17:06):

meanwhile you can probably do something like what's done in mathcomp CI to test the master version of analysis: https://github.com/math-comp/math-comp/blob/master/.nix/config.nix (mind the mathcomp-classical overlay in .nix/coq-overlays)

view this post on Zulip Cyril Cohen (Feb 01 2024 at 17:07):

Florent Hivert said:

Did you just did it ? Or did the fact that I wrote

    coqPackages.mathcomp-classical.override.version = "1.0.0";

solve the problem using

 /nix/store/1bcyd7v30is0ii8h81drd92sxiycjzyr-coq8.19-mathcomp2.2-mathcomp-classical-dev

It would probably solve your problem indeed.

view this post on Zulip Florent Hivert (Feb 01 2024 at 17:20):

@Pierre Roux @Cyril Cohen : CI seems to be properly working now ! Thanks for the help !


Last updated: Jul 15 2024 at 21:02 UTC