CI : nano not found · Coq users · Zulip Chat Archive

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

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

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

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!

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

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

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 :-(

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).

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

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?

Stream: Coq users

Topic: CI : nano not found

Laurent Théry (Jun 29 2023 at 12:00):