Stream: Coq users

Topic: CI : nano not found


view this post on Zulip Laurent Théry (Jun 29 2023 at 12:00):

I am trying to set up a CI on a coq github repository with meta.yml but it is failling with the message

sh: 1: nano: not found

what did I do wrong?

view this post on Zulip Paolo Giarrusso (Jun 29 2023 at 12:18):

IIUC, Opam cannot find coq-expfloat.opam package file — No valid package definition found is the more relevant error

+ (script @ line 10) $ opam pin add -n -y -k path coq-expfloat .
  Package coq-expfloat does not exist, create as a NEW package? [Y/n] y
  [coq-expfloat.~dev] synchronised (file:///github/workspace)
  [NOTE] No package definition found for coq-expfloat.~dev: please complete the template
  sh: 1: nano: not found
  Error:  Empty file or editor error, aborting.
  Error:  No valid package definition found

view this post on Zulip Paolo Giarrusso (Jun 29 2023 at 12:19):

I'm sure opam doesn't know anything about meta.yml, not sure if any meta.yml infrastructure would generate the opam packages

view this post on Zulip Laurent Théry (Jun 29 2023 at 12:20):

ok thanks I forgot to add the opam file that was generated to my repo. Thanks a lot!

view this post on Zulip Laurent Théry (Jun 29 2023 at 12:23):

Ok that was the problem. Thanks. Anyway this nano message is a bit disturbing.... Thanks again

view this post on Zulip Paolo Giarrusso (Jun 29 2023 at 12:55):

"disturbing"? Just to avoid misunderstandings, opam is trying to call command-line editor https://www.nano-editor.org/ , but that's not installed in CI images, hence the shell sh is telling sh: 1: nano: not found

view this post on Zulip Paolo Giarrusso (Jun 29 2023 at 12:59):

not sure what that message seems like otherwise!
maybe opam should support a --no-interactive option, but I can't find an existing one (maybe --confirm-level). Unfortunately seems very low priority, but what do I know :-(

view this post on Zulip Enrico Tassi (Jun 29 2023 at 13:18):

I think unsetting the EDITOR variable may be enough. Or set it to an actual editor (but then the CI job would probably stall).

view this post on Zulip Karl Palmskog (Jun 29 2023 at 13:42):

this looks like a new behavior for recent opam. We'll have to investigate if there's an option to avoid the "complete the template" part, so no editor is invoked

view this post on Zulip Paolo Giarrusso (Jun 29 2023 at 14:10):

Either way, docker-coq-action could test if $pkg.opam exists (here coq-expfloat.opam — it knows the name!) and give a better error if not?

view this post on Zulip Karl Palmskog (Jun 29 2023 at 14:11):

right, in the end this is a Docker-Coq-Action issue. Could someone report it there as memento? https://github.com/coq-community/docker-coq-action/issues


Last updated: Jun 13 2024 at 19:02 UTC