bug#39020: closed (Lean won't work with the emacs mode)

[GNU bug Tracking System]

Your message dated Mon, 13 Jan 2020 16:00:03 -0600
with message-id <address@hidden>
and subject line Re: [bug#39020] Lean won't work with the emacs mode
has caused the debbugs.gnu.org bug report #39020,
regarding Lean won't work with the emacs mode
to be marked as done.

(If you believe you have received this mail in error, please contact
address@hidden.)


-- 
39020: http://debbugs.gnu.org/cgi/bugreport.cgi?bug=39020
GNU Bug Tracking System
Contact address@hidden with problems
> --- Begin Message ---
>
>
>
> Subject: 
>
> Lean won't work with the emacs mode
>
>
>
>
> Date: 
>
> Tue, 07 Jan 2020 19:53:49 +0100
>
>
>
>
> User-agent: 
>
> Evolution 3.30.5 (3.30.5-1.fc29) 
>
>
>
>
> The emacs mode for Lean (which doesn't appear to be packaged yet, but
> of course works via MELPA etc.) expects some sort of root directory for
> Lean, which is not given simply because binaries and other files are
> put into separate directories. This of course makes Lean impossible to
> use as intended. However, I'm not quite sure how this would be fixed in
> practice, as I'm not aware of any suitable directory hierarchy in such
> a case.
>
> Any ideas?
>
> --
>
> Arvid
>
>
>
>
> --- End Message ---
> --- Begin Message ---
>
>
>
> Subject: 
>
> Re: [bug#39020] Lean won't work with the emacs mode
>
>
>
>
> Date: 
>
> Mon, 13 Jan 2020 16:00:03 -0600
>
>
>
>
> User-agent: 
>
> Gnus/5.13 (Gnus v5.13) Emacs/26.3 (gnu/linux)
>
>
>
>
> Arvid Marx <address@hidden> writes:
>
> > Maxim Cournoyer wrote:
> >> Hello Arvid,
> >> 
> >> [...]
> >> When writing the package definition for the Emacs Lead mode, the code
> >> could be rewritten to refer to the absolute path of the
> >> files/programs
> >> it uses from the Lean project, by patching it with `substitute*'
> >> uses,
> >> for example.
> >> 
> >> If that is not easy to do, another idea would be to create some kind
> >> of
> >> overlay directory which would flatly collect all the items needed
> >> then
> >> refer to that (the items would be symlinked to their real location).
> >> See the `union-build' procedure of the (guix build union) module of
> >> Guix.
> >> 
> >> HTH!
> >> 
> >> Maxim
> >
> > Hello Maxim,
> >
> > thanks for your response! The second idea is basically what I had in
> > mind, as the Lean mode seems to depend on an actual file tree. Patching
> > the emacs mode however looks quite simple, as all one needed to do is
> > change the definition of lean-get-executable as defined in 
> > https://raw.githubusercontent.com/leanprover/lean-mode/master/lean-util.el
> > . I might take a closer look and write a simple patch at some point,
> > but up to that point, it appears that just using ~/.guix-profile as a
> > root directory works as well, or at least doesn't raise any errors when
> > type checking etc.
> >
> > Again, thanks for feedback!
> >
> > --
> >
> > Arvid 
> >
> >
> >
> >
> >
>
> Closing.
>
> -- 
> Brett M. Gilio
> GNU Guix, Contributor | GNU Project, Webmaster
> [DFC0 C7F7 9EE6 0CA7 AE55 5E19 6722 43C4 A03F 0EEE]
> <address@hidden> <address@hidden>
>
>
> --- End Message ---