[CakeML-Dev] FW: Holmakefile hacking

[Ramana Kumar]

By the way, even if you write the initial version of this in Python, I
think it should eventually be written in ML (standard or preferably cake).
Our verified libraries should eventually become good enough to support such
applications easily.

On 11 November 2016 at 16:33, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>
wrote:

> I think this should have been sent to developers at cakeml.org by the way -
> was it dev on purpose?
>
> On 11 November 2016 at 16:17, Magnus Myreen <magnus.myreen at gmail.com>
> wrote:
>
>> Thanks!
>>
>> On Fri, 11 Nov 2016 at 06:14, <Michael.Norrish at data61.csiro.au> wrote:
>>
>>> (Realised that my original reply only went to Magnus.)
>>>
>>> As with all Makefiles, the indentation in the Makefile rules has to be a
>>> TAB character.
>>>
>>> Michael
>>>
>>> On 11/11/16, 16:12, "Norrish, Michael (Data61, Canberra City)" <
>>> Michael.Norrish at data61.csiro.au> wrote:
>>>
>>>     Sure.  One approach would be to add something like
>>>
>>>     Foo.doc: FooScript.sml
>>>         python ../../dev/generate_readme.py < $< > $@
>>>
>>>     for every script file in the directory.
>>>
>>>     Alternatively, it might be slightly annoying to have to write one
>>> such rule for every such script file, so you could also do the slightly
>>> hacky:
>>>
>>>     DOC_SOURCES = $(wildcard *Script.sml)
>>>     DOC_TARGETS = $(patsubst %Script.sml,%.doc,$(DOC_SOURCES))
>>>
>>>     all: $(DOC_TARGETS)
>>>     .PHONY: all
>>>
>>>
>>>     $(DOC_TARGETS): $(DOC_SOURCES)
>>>         python ../../dev/generate_readme.py < $(patsubst
>>> %.doc,%Script.sml,$@) > $@
>>>
>>>     the hackiness here comes from the fact that every .doc file is held
>>> to depend on all the scripts, so that if you change 1 script file, all of
>>> the doc-files will get rebuilt.  (Using wildcard isn’t great style
>>> either.)  Assuming the doc-generator is quick, this shouldn’t be a
>>> practical issue though.
>>>
>>>     I hope this helps.  I’ve tested it (using head -10 instead of a
>>> python program), and it seems to behave the right way.
>>>
>>>     Michael
>>>
>>>     On 11/11/16, 15:52, "Magnus Myreen" <magnus.myreen at gmail.com> wrote:
>>>
>>>         Hi Michael,
>>>
>>>         Quick question, you wrote the following under
>>>         https://github.com/CakeML/cakeml/issues/71
>>>
>>>             The right way to do this would be to write a tool that
>>>             generates these from the script files, and to then have the
>>>             directory's Holmakefile try to generate one such in every
>>>             directory.
>>>
>>>         I might write the tool during one of my flights, and I wonder
>>>         what the right rule looks like in the Holmakefile.
>>>
>>>         Could you provide me with a snippet of Holmakefile code that runs
>>>         my tool, say, invoked by python ../../dev/generate_readme.py ?
>>>
>>>         Thanks!
>>>
>>>         Cheers,
>>>         Magnus
>>>
>>>
>>>
>>>
>>>
>>> _______________________________________________
>>> Dev mailing list
>>> Dev at cakeml.org
>>> https://lists.cakeml.org/listinfo/dev
>>>
>>
>> _______________________________________________
>> Dev mailing list
>> Dev at cakeml.org
>> https://lists.cakeml.org/listinfo/dev
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20161111/b7ee7419/attachment.html>