* ocaml-stdlib-shims: setting paths for a Coq package
@ 2023-09-02 18:52 Garek Dyszel
2023-09-03 16:02 ` Julien Lepiller
0 siblings, 1 reply; 3+ messages in thread
From: Garek Dyszel @ 2023-09-02 18:52 UTC (permalink / raw)
To: help-guix
Hi Guix,
While trying to package coq-elpi, one finds that Findlib is unable to
find ocaml-stdlib-shims. The problem persists even if ocaml-stdlib-shims
is located in the inputs and propagated-inputs fields.
Trying to set OCAMLLIB using the following doesn't seem to work.
(string-append "OCAMLLIB=$OCAMLLIB:"
#$(this-package-input "ocaml-stdlib-shims"))
Which environment variable should we be setting so that
ocaml-stdlib-shims can be picked up by Coq?
I can include the whole package file from which this question is
originating if it would help, but there are about 20 packages in there;
I don't want to force anybody to read it unless we really have to :)
Garek
Make flags for coq-elpi
--8<---------------cut here---------------start------------->8---
;; Most of the package definition omitted...
(arguments ;;...
`(#:make-flags ,#~(list (string-append "COQBIN="
#$(this-package-input "coq-core")
"/bin/")
(string-append "ELPIDIR="
#$(this-package-input "ocaml-elpi")
"/lib/ocaml/site-lib/elpi")
(string-append "COQLIBINSTALL="
#$output
"/lib/coq/user-contrib")
(string-append "COQMF_COQLIB="
#$output
"/lib/ocaml/site-lib/coq")
(string-append "OCAMLLIB=$OCAMLLIB:"
#$(this-package-input
"ocaml-stdlib-shims"))
(string-append "COQPLUGININSTALL="
#$output
"/lib/ocaml/site-lib")
"OCAMLWARN=")
;;...
))
--8<---------------cut here---------------end--------------->8---
Adjusted arguments for ocaml-stdlib-shims (adding the phase install-meta
doesn't seem to fix the problem)
--8<---------------cut here---------------start------------->8---
(define-public ocaml-stdlib-shims
(package
(name "ocaml-stdlib-shims")
(version "0.3.0")
(source (origin
(method git-fetch)
(uri (git-reference
(url "https://github.com/ocaml/stdlib-shims")
(commit version)))
(file-name (git-file-name name version))
(sha256
(base32
"0gmg8w67j3ww17llk7hl4dx0vq7p50rn5s4ib9sy984k543rz59h"))))
(build-system dune-build-system)
(arguments
`(#:phases
(modify-phases %standard-phases
(delete 'configure)
(add-after 'install 'install-meta
(lambda* (#:key outputs #:allow-other-keys)
(let ((out (assoc-ref outputs "out")))
(with-output-to-file
(string-append out "/lib/ocaml/site-lib/stdlib-shims/META")
(lambda _
(display
"package \"stdlib-shims\" (
description = \"Stdlib shims\"
requires = \"\"
archive(byte) = \"stdlib_shims.cma\"
archive(native) = \"stdlib_shims.cmxa\"
plugin(byte) = \"stdlib_shims.cma\"
plugin(native) = \"stdlib_shims.cmxs\"
)")))))))))
(home-page "https://github.com/ocaml/stdlib-shims")
(synopsis "OCaml stdlib features backport to older OCaml compilers")
(description "This package backports some of the new stdlib features to
older compilers, such as the Stdlib module. This allows projects that require
compatibility with older compiler to use these new features in their code.")
;; with ocaml-linking exception
(license license:lgpl2.1+)))
--8<---------------cut here---------------end--------------->8---
^ permalink raw reply [flat|nested] 3+ messages in thread
* Re: ocaml-stdlib-shims: setting paths for a Coq package
2023-09-02 18:52 ocaml-stdlib-shims: setting paths for a Coq package Garek Dyszel
@ 2023-09-03 16:02 ` Julien Lepiller
0 siblings, 0 replies; 3+ messages in thread
From: Julien Lepiller @ 2023-09-03 16:02 UTC (permalink / raw)
To: help-guix, Garek Dyszel
Le 2 septembre 2023 20:52:21 GMT+02:00, Garek Dyszel <garekdyszel@disroot.org> a écrit :
>Hi Guix,
>
>While trying to package coq-elpi, one finds that Findlib is unable to
>find ocaml-stdlib-shims. The problem persists even if ocaml-stdlib-shims
>is located in the inputs and propagated-inputs fields.
>
>Trying to set OCAMLLIB using the following doesn't seem to work.
>(string-append "OCAMLLIB=$OCAMLLIB:"
> #$(this-package-input "ocaml-stdlib-shims"))
>
>Which environment variable should we be setting so that
>ocaml-stdlib-shims can be picked up by Coq?
>
>I can include the whole package file from which this question is
>originating if it would help, but there are about 20 packages in there;
>I don't want to force anybody to read it unless we really have to :)
>
>Garek
>
>
>Make flags for coq-elpi
>--8<---------------cut here---------------start------------->8---
>;; Most of the package definition omitted...
>(arguments ;;...
>`(#:make-flags ,#~(list (string-append "COQBIN="
> #$(this-package-input "coq-core")
> "/bin/")
> (string-append "ELPIDIR="
> #$(this-package-input "ocaml-elpi")
> "/lib/ocaml/site-lib/elpi")
> (string-append "COQLIBINSTALL="
> #$output
> "/lib/coq/user-contrib")
> (string-append "COQMF_COQLIB="
> #$output
> "/lib/ocaml/site-lib/coq")
> (string-append "OCAMLLIB=$OCAMLLIB:"
> #$(this-package-input
> "ocaml-stdlib-shims"))
> (string-append "COQPLUGININSTALL="
> #$output
> "/lib/ocaml/site-lib")
> "OCAMLWARN=")
> ;;...
> ))
>--8<---------------cut here---------------end--------------->8---
>
>Adjusted arguments for ocaml-stdlib-shims (adding the phase install-meta
>doesn't seem to fix the problem)
>--8<---------------cut here---------------start------------->8---
>(define-public ocaml-stdlib-shims
> (package
> (name "ocaml-stdlib-shims")
> (version "0.3.0")
> (source (origin
> (method git-fetch)
> (uri (git-reference
> (url "https://github.com/ocaml/stdlib-shims")
> (commit version)))
> (file-name (git-file-name name version))
> (sha256
> (base32
> "0gmg8w67j3ww17llk7hl4dx0vq7p50rn5s4ib9sy984k543rz59h"))))
> (build-system dune-build-system)
> (arguments
> `(#:phases
> (modify-phases %standard-phases
> (delete 'configure)
> (add-after 'install 'install-meta
> (lambda* (#:key outputs #:allow-other-keys)
> (let ((out (assoc-ref outputs "out")))
> (with-output-to-file
> (string-append out "/lib/ocaml/site-lib/stdlib-shims/META")
> (lambda _
> (display
> "package \"stdlib-shims\" (
> description = \"Stdlib shims\"
> requires = \"\"
> archive(byte) = \"stdlib_shims.cma\"
> archive(native) = \"stdlib_shims.cmxa\"
> plugin(byte) = \"stdlib_shims.cma\"
> plugin(native) = \"stdlib_shims.cmxs\"
> )")))))))))
> (home-page "https://github.com/ocaml/stdlib-shims")
> (synopsis "OCaml stdlib features backport to older OCaml compilers")
> (description "This package backports some of the new stdlib features to
>older compilers, such as the Stdlib module. This allows projects that require
>compatibility with older compiler to use these new features in their code.")
> ;; with ocaml-linking exception
> (license license:lgpl2.1+)))
>--8<---------------cut here---------------end--------------->8---
>
Hi Garek,
It should work with OCAMLPATH, not OCAMLLIB. If you use the ocaml-build-system or the dune-build-system, it should already be set. Otherwise, adding ocaml to your native-inputs should help.
^ permalink raw reply [flat|nested] 3+ messages in thread
* Re: ocaml-stdlib-shims: setting paths for a Coq package
@ 2023-09-04 16:37 Garek Dyszel
0 siblings, 0 replies; 3+ messages in thread
From: Garek Dyszel @ 2023-09-04 16:37 UTC (permalink / raw)
To: Julien Lepiller; +Cc: help-guix
Hi Julien,
It looks like setting OCAMLLIB or OCAMLPATH has no effect on whether Coq
is able to find stdlib-shims. I built coq-elpi after including one of
each and then both together, and none of those three configurations
changed whether coq-elpi could find ocaml-stdlib-shims.
I tried adding ocaml-stdlib-shims to COQPATH with the following line.
The path to ocaml-stdlib-shims doesn't show up in COQPATH; am I adding
it incorrectly here?
(string-append "COQPATH=$COQPATH:"
#$(this-package-input
"ocaml-stdlib-shims")
"/lib/ocaml/site-lib/stdlib-shims")
It seems like the general idea of adding this input to COQPATH would
work, but it's not possible to test the idea just yet...
Thanks for the help!
Garek
^ permalink raw reply [flat|nested] 3+ messages in thread
end of thread, other threads:[~2023-09-06 9:38 UTC | newest]
Thread overview: 3+ messages (download: mbox.gz follow: Atom feed
-- links below jump to the message on this page --
2023-09-02 18:52 ocaml-stdlib-shims: setting paths for a Coq package Garek Dyszel
2023-09-03 16:02 ` Julien Lepiller
-- strict thread matches above, loose matches on Subject: below --
2023-09-04 16:37 Garek Dyszel
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).