[CakeML-Dev] Holmakefile hacking

[Michael.Norrish at data61.csiro.au]

Agreed.  The write-in-SML and compile-with-polyc experience is not so awful either.

Michael

From: Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>
Date: Friday, 11 November 2016 at 16:43
To: Magnus Myreen <magnus.myreen at gmail.com>
Cc: "Norrish, Michael (Data61, Canberra City)" <Michael.Norrish at data61.csiro.au>, "developers at cakeml.org" <developers at cakeml.org>
Subject: Re: FW: Holmakefile hacking

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<mailto:Ramana.Kumar at cl.cam.ac.uk>> wrote:
I think this should have been sent to developers at cakeml.org<mailto: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<mailto:magnus.myreen at gmail.com>> wrote:
Thanks!

On Fri, 11 Nov 2016 at 06:14, <Michael.Norrish at data61.csiro.au<mailto: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<mailto: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<mailto: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<mailto:Dev at cakeml.org>
https://lists.cakeml.org/listinfo/dev

_______________________________________________
Dev mailing list
Dev at cakeml.org<mailto: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/f82ea53c/attachment-0001.html>