make less coq stuff about unimath HOT 7 CLOSED

Hmm? How is that less? It looks like more.

from unimath.

On 09/28/2015 03:12 PM, Daniel R. Grayson wrote:

Hmm? How is that less? It looks like more.

From Makefile.build:

coqlight: theories-light tools coqbinaries

from unimath.

I suppose you're talking about changing these lines in our Makefile:

sub/coq/bin/coq_makefile sub/coq/bin/coqc: sub/coq/config/coq_config.ml
    $(MAKE) -C sub/coq KEEP_ML4_PREPROCESSED=true VERBOSE=true READABLE_ML4=yes coqlight
sub/coq/bin/coqide: sub/lablgtk/README sub/coq/config/coq_config.ml
    $(MAKE) -C sub/coq KEEP_ML4_PREPROCESSED=true VERBOSE=true READABLE_ML4=yes coqide-binaries bin/coqide

Are you suggesting replacing coqlight by coqbinaries tools? If so, did you test it?

I remember looking for something more minimal than coqlight and not finding a good target.

from unimath.

On 09/28/2015 04:08 PM, Daniel R. Grayson wrote:

I suppose you're talking about changing these lines in our Makefile:

sub/coq/bin/coq_makefile sub/coq/bin/coqc: sub/coq/config/coq_config.ml
  $(MAKE) -C sub/coq KEEP_ML4_PREPROCESSED=true VERBOSE=true READABLE_ML4=yes coqlight
sub/coq/bin/coqide: sub/lablgtk/README sub/coq/config/coq_config.ml
  $(MAKE) -C sub/coq KEEP_ML4_PREPROCESSED=true VERBOSE=true READABLE_ML4=yes coqide-binaries bin/coqide

Are you suggesting replacing coqlight by coqbinaries tools? If so, did you test it?

No testing done yet, I was merely recording an idea, maybe to be
implemented during a UniMath day.

from unimath.

Actually, the three

• coqbinaries
• tools
• theories/Init/Prelude.vo (to provide the prelude)

are necessary, which is a bit less than coqlight.

from unimath.

Solved with #170

from unimath.

If your commit message had said "resolves #170" instead of "see #170" this issue would have been closed automagically by github.

from unimath.