Re: Summary and next steps for (package-initialize)

[Radon Rosborough]

> From: Radon Rosborough <address@hidden>
> Date: Mon, 21 Aug 2017 13:33:51 -0700
> Cc: address@hidden
>
> > That being said, one possibility is to have a function in package.el
> > scan the user init file for the definition of package-load-list, and
> > process that line before loading the packages.
>
> I really don't want to sound rude, but... *please* no. That would be a
> horrible hack.

We do something very similar in other situations, like finding the
file-local variables.

> It will fail in so many different circumstances:
> package-load-list set in a different file, package-load-list set
> dynamically, package-load-list set in an unconventional way,
> package-load-list set by a macro, etc. etc. etc.

Nothing that cannot be handled.

> Emacs Lisp is Turing-complete. It is futile for Emacs to try to
> understand it.

That's a strange thing to say about a program which implements that
very language.

Anyway, the proposal still stays, and I just pointed out one way,
perhaps not the best one, out of the conundrum that you described as
insoluble.  I hope someone will come up with a better solution, or
implement what I proposed.  Otherwise, I predict that we will remain
at an impasse for some time more.

=====

> > > That being said, one possibility is to have a function in package.el
> > > scan the user init file for the definition of package-load-list, and
> > > process that line before loading the packages.
> >
> > I really don't want to sound rude, but... *please* no. That would be a
> > horrible hack.
>
> We do something very similar in other situations, like finding the
> file-local variables.

That is completely different. File-local variables conform to a fixed,
simple syntax which is -- in particular -- not Turing-complete, unlike
Emacs Lisp.

If you'd like to propose that `package-load-list' and friends only be
settable via file-local variables, then that would indeed solve the
problem. But that's a different proposal.

> > Emacs Lisp is Turing-complete. It is futile for Emacs to try to
> > understand it.
>
> That's a strange thing to say about a program which implements that
> very language.

I should have said: "Emacs Lisp is Turing-complete. It is futile for
Emacs to try to understand it in any way other than executing it."
That is what I meant. Static analysis is very different from just
running the program and seeing what happens.

> > It will fail in so many different circumstances:
> > package-load-list set in a different file, package-load-list set
> > dynamically, package-load-list set in an unconventional way,
> > package-load-list set by a macro, etc. etc. etc.
>
> Nothing that cannot be handled.

This is objectively false, and can be formally proven as such. I'll
try to explain better this time. (But the gist is, if you could
somehow "handle" this in general, you would also be able to solve the
halting problem.)

The issue is that determining anything nontrivial about the behavior
of an arbitrary piece of code is impossible in general, if the
language is Turing-complete. This is the content of Rice's theorem.
Stated in terms of Turing machines, it is as follows:

    Let S be a property of Turing machines. Assume that S is a
    nontrivial property, meaning that there exists at least one Turing
    machine with property S and at least one Turing machine without
    property S. Assume also that S is a functional property, meaning
    that it depends only on the inputs accepted and rejected by the
    Turing machine. Then, it is undecidable whether an arbitrary
    Turing machine has property S.

Stated in terms of package.el:

    Let S be a property of Emacs Lisp init-files. In particular, let S
    be the property that `package-load-list' is set to a given value T
    when the init-file is evaluated. It can be verified that the
    property S is nontrivial and functional. Thus, it is undecidable
    whether an arbitrary Emacs Lisp init-file sets `package-load-list'
    to any given value.

There is a loophole, however, since in the case of init-files, we are
willing to limit ourself to the case where running the code is
guaranteed to terminate (otherwise Emacs would not start up in the
first place).

This allows us to determine, in general, what an init-file does to
`package-load-list'. The catch is that we must actually evaluate the
init-file to do so. Why is this important?

It means that we can't correctly figure out the values of
`package-load-list' and `package-user-dir' before we have actually
loaded the init-file. It is only possible to do a `package-initialize'
operation correctly *after* loading the init-file, and any attempt to
the contrary will fail in general.

> Anyway, the proposal still stays

OK, but given that there is a formal proof that no general solution
can possibly exist, I don't think anybody will find one. If you're
proposing that we simply accept that package.el cannot be customized
in a dynamic way, then yes, that would solve the problem. But that's a
different proposal.

> I just pointed out one way, perhaps not the best one, out of the
> conundrum that you described as insoluble.

Your way relies on solving the halting problem. I don't think it
counts.

> I hope someone will come up with a better solution, or implement
> what I proposed. Otherwise, I predict that we will remain at an
> impasse for some time more.

I started this thread by proposing a specific, comprehensive solution
to the problem. Nobody has pointed out any flaws yet. Why is there an
impasse?

Best,
Radon

P.S. Sorry if I'm being a bit blunt here. But it's hard not to be
blunt in analyzing a problem when computability theory says there is
no solution.