> On Jul 10, 2020, at 11:55 PM, Yozo TODA <[email protected]> wrote:
>
> -----BEGIN PGP SIGNED MESSAGE-----
> Hash: SHA256
>
>>> One patch is no longer needed as it seemsto have been upstreamed.
>>>
>>> Continues to work for me on amd64 (as does CompCert).
>>>
>>> ok?
>>
>> OK
>
> me too :-D
Thanks. Will commit shortly. Some additional notes below if you’d like to
consider some further coq improvements :-)
> it compiles on amd64, and testing going on...
1) Most of the regress tests on amd64 pass for me btw. But it would be really
nice to investigate the failing ones if they are expected or not. There were a
handful of failures on my end.
2) I’ve recently re-enabled compcert builds on aarch64 and powerpc. This will
give us somewhat of a basic runtime rest of coq on those platforms. on aarch64
it looks like coq builds but doesn’t actually run. See the compcert logs which
show this:
http://build-failures.rhaalovely.net/aarch64/2020-07-08/lang/compcert.log
>
> BTW,
>
>>> +lib/ocaml/coq/doc/
>>> +lib/ocaml/coq/doc/tools/
>>> +lib/ocaml/coq/doc/tools/docgram/
>
> docgram directory is empty.
> it should be removed? or put README.md and other files here?
Here I believe I just ran the standard “make fake” followed by “make plist”.
So either I botched something on my end, or coq doesn’t install those files as
expected.
Probably worth investigating. We can update in a future revision if anything
needs to change.
>
> % ls -l /usr/ports/pobj/coq*/coq*/doc/tools/docgram/
> total 644
> - -rw-r--r-- 1 yozo wheel 8953 May 15 05:29 README.md
> - -rw-r--r-- 1 yozo wheel 5195 May 15 05:29 common.edit_mlg
> - -rw-r--r-- 1 yozo wheel 28253 Jul 11 11:22 doc_grammar.cmi
> - -rw-r--r-- 1 yozo wheel 65776 Jul 11 11:22 doc_grammar.cmo
> - -rw-r--r-- 1 yozo wheel 57373 May 15 05:29 doc_grammar.ml
> - -rw-r--r-- 1 yozo wheel 69848 May 15 05:29 fullGrammar
> - -rw-r--r-- 1 yozo wheel 80158 May 15 05:29 orderedGrammar
> - -rw-r--r-- 1 yozo wheel 830 May 15 05:29 prodn.edit_mlg
> - -rw-r--r-- 1 yozo wheel 1088 May 15 05:29 productionlist.edit_mlg
are they also installed in fake?
