<div dir="ltr">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.<br></div><div class="gmail_extra"><br><div class="gmail_quote">On 11 November 2016 at 16:33, Ramana Kumar <span dir="ltr"><<a href="mailto:Ramana.Kumar@cl.cam.ac.uk" target="_blank">Ramana.Kumar@cl.cam.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">I think this should have been sent to <a href="mailto:developers@cakeml.org" target="_blank">developers@cakeml.org</a> by the way - was it dev on purpose?<br></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On 11 November 2016 at 16:17, Magnus Myreen <span dir="ltr"><<a href="mailto:magnus.myreen@gmail.com" target="_blank">magnus.myreen@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Thanks!<div class="m_2623124435157935747HOEnZb"><div class="m_2623124435157935747h5"><br><div class="gmail_quote"><div dir="ltr">On Fri, 11 Nov 2016 at 06:14, <<a href="mailto:Michael.Norrish@data61.csiro.au" target="_blank">Michael.Norrish@data61.csiro.<wbr>au</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">(Realised that my original reply only went to Magnus.)<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
As with all Makefiles, the indentation in the Makefile rules has to be a TAB character.<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
Michael<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
On 11/11/16, 16:12, "Norrish, Michael (Data61, Canberra City)" <<a href="mailto:Michael.Norrish@data61.csiro.au" class="m_2623124435157935747m_2170977484925476333gmail_msg" target="_blank">Michael.Norrish@data61.csiro.<wbr>au</a>> wrote:<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
Sure. One approach would be to add something like<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
Foo.doc: FooScript.sml<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
python ../../dev/generate_readme.py < $< > $@<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
for every script file in the directory.<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
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:<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
DOC_SOURCES = $(wildcard *Script.sml)<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
DOC_TARGETS = $(patsubst %Script.sml,%.doc,$(DOC_SOURCE<wbr>S))<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
all: $(DOC_TARGETS)<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
.PHONY: all<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
$(DOC_TARGETS): $(DOC_SOURCES)<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
python ../../dev/generate_readme.py < $(patsubst %.doc,%Script.sml,$@) > $@<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
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.<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
I hope this helps. I’ve tested it (using head -10 instead of a python program), and it seems to behave the right way.<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
Michael<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
On 11/11/16, 15:52, "Magnus Myreen" <<a href="mailto:magnus.myreen@gmail.com" class="m_2623124435157935747m_2170977484925476333gmail_msg" target="_blank">magnus.myreen@gmail.com</a>> wrote:<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
Hi Michael,<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
Quick question, you wrote the following under<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
<a href="https://github.com/CakeML/cakeml/issues/71" rel="noreferrer" class="m_2623124435157935747m_2170977484925476333gmail_msg" target="_blank">https://github.com/CakeML/cake<wbr>ml/issues/71</a><br class="m_2623124435157935747m_2170977484925476333gmail_msg">
<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
The right way to do this would be to write a tool that<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
generates these from the script files, and to then have the<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
directory's Holmakefile try to generate one such in every<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
directory.<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
I might write the tool during one of my flights, and I wonder<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
what the right rule looks like in the Holmakefile.<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
Could you provide me with a snippet of Holmakefile code that runs<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
my tool, say, invoked by python ../../dev/generate_readme.py ?<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
Thanks!<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
Cheers,<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
Magnus<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
______________________________<wbr>_________________<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
Dev mailing list<br class="m_2623124435157935747m_2170977484925476333gmail_msg">
<a href="mailto:Dev@cakeml.org" class="m_2623124435157935747m_2170977484925476333gmail_msg" target="_blank">Dev@cakeml.org</a><br class="m_2623124435157935747m_2170977484925476333gmail_msg">
<a href="https://lists.cakeml.org/listinfo/dev" rel="noreferrer" class="m_2623124435157935747m_2170977484925476333gmail_msg" target="_blank">https://lists.cakeml.org/listi<wbr>nfo/dev</a><br class="m_2623124435157935747m_2170977484925476333gmail_msg">
</blockquote></div>
</div></div><br>______________________________<wbr>_________________<br>
Dev mailing list<br>
<a href="mailto:Dev@cakeml.org" target="_blank">Dev@cakeml.org</a><br>
<a href="https://lists.cakeml.org/listinfo/dev" rel="noreferrer" target="_blank">https://lists.cakeml.org/listi<wbr>nfo/dev</a><br>
<br></blockquote></div><br></div>
</div></div></blockquote></div><br></div>