<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class=""><div class="">Thought it may be helpful to show the current directory structure (below). I have a preference for compiler/targets/x64 over compiler/x64, especially if the new targets/ directory did actually contain all of the target specific stuff. - Anthony</div><div class=""><br class=""></div><div class=""><div style="margin: 0px; font-size: 12px; line-height: normal; font-family: Menlo; background-color: rgb(255, 255, 255);" class=""><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">.</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">├── backend</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">│ ├── bignum</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">│ ├── gc</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">│ ├── proofs</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">│ ├── reg_alloc</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">│ │ └── proofs</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">│ └── semantics</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">├── bootstrap</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">│ ├── evaluation</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">│ ├── io</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">│ └── translation</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">├── eval</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">│ ├── benchmarks</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">│ │ ├── cakeml</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">│ │ ├── ocaml</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">│ │ └── poly</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">│ │ └── other</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">│ ├── other_benchmarks</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">│ │ └── cakeml</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">│ │ ├── arm</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">│ │ ├── arm8</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">│ │ ├── mips</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">│ │ ├── riscv</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">│ │ └── x64</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">│ ├── targets</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">│ │ └── proofs</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">│ └── x64</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">├── inference</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">│ └── proofs</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">├── parsing</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">│ ├── proofs</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">│ └── testing</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">├── proofs</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class="">└── targets</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""> ├── all</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""> ├── arm6</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""> │ └── proofs</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""> ├── arm8</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""> │ └── proofs</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""> ├── asm</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""> ├── mips</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""> │ └── proofs</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""> ├── riscv</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""> │ └── proofs</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""> └── x64</span></div><div style="margin: 0px; line-height: normal;" class=""><span style="font-variant-ligatures: no-common-ligatures" class=""> └── proofs</span></div></div></div><div class=""><span style="font-variant-ligatures: no-common-ligatures" class=""><br class=""></span></div><br class=""><div><blockquote type="cite" class=""><div class="">On 19 Dec 2016, at 23:46, Yong Kiam <<a href="mailto:tanyongkiam@gmail.com" class="">tanyongkiam@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class="">Your plan combined with Magnus' sound good. We could finalise the sketching at the next hangout in case anyone has other suggestions, or has things to point out.<br class=""></div><div class="gmail_extra"><br class=""><div class="gmail_quote">On Mon, Dec 19, 2016 at 5:04 PM, Ramana Kumar <span dir="ltr" class=""><<a href="mailto:Ramana.Kumar@cl.cam.ac.uk" target="_blank" class="">Ramana.Kumar@cl.cam.ac.uk</a>></span> wrote:<br class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Yong Kiam, developers,<br class="">
<br class="">
I think this discussion should happen on the Developers list, so I've<br class="">
changed the CC.<br class="">
<br class="">
I like Magnus's latest suggestion with regards to the targets/config<br class="">
organisation.<br class="">
<br class="">
I would like the eval directory to be deleted. If we move to<br class="">
compiler/benchmarks and compiler/x64 etc. then the only thing left in<br class="">
eval is the compiler compute lib. This, I think, could be split and<br class="">
left as a single file in various directories, e.g.,<br class="">
compiler/backend/<wbr class="">backendComputeLib.sml, as well as a full merged<br class="">
version in compiler/compilerComputeLib.<wbr class="">sml. Does that sound OK?<br class="">
<br class="">
I think the directory organisation is rather complex (since there are<br class="">
a lot of things, and non-trivial dependencies), and it might be<br class="">
worthwhile sketching a full plan of where we're moving to on the wiki<br class="">
(e.g., on the Conventions page) to run across all the potential<br class="">
problems before you start moving files around. It's up to you how you<br class="">
want to work on it, though :)<br class="">
<br class="">
Cheers,<br class="">
Ramana<br class="">
<div class="HOEnZb"><div class="h5"><br class="">
On 20 December 2016 at 08:08, Magnus Myreen <<a href="mailto:magnus.myreen@gmail.com" class="">magnus.myreen@gmail.com</a>> wrote:<br class="">
> I take back my previous suggestion regarding compiler/targets, because<br class="">
> I think the file organisation I suggested is confusing.<br class="">
><br class="">
> Here's another file organisation:<br class="">
><br class="">
> compiler/x64<br class="">
> is where the instantiation of the top-level compiler to x64 should<br class="">
> live, including its config, also exportLib for x64<br class="">
><br class="">
> compiler/x64/proofs<br class="">
> a proof of config_ok for x64 and an instantiation of the top-level<br class="">
> compiler thm<br class="">
><br class="">
> compiler/x64/encoder and compiler/x64/encoder/proofs<br class="">
> is what is currently under targets/x64<br class="">
><br class="">
> The definition of asm and other common infrastructure under<br class="">
> compiler/targets could move under compiler/backend/asm.<br class="">
><br class="">
> I suspect this file organisation is more intuitive for people new to<br class="">
> the code base. If one wants to find the x64 version of the compiler<br class="">
> one dives into compiler and then into x64, and one finds it. If one<br class="">
> wants to find the proofs about it, one then dives into proofs and one<br class="">
> gets to see a short file that opens various important files that one<br class="">
> can then find my chasing the includes.<br class="">
><br class="">
> Comments on this suggestion?<br class="">
><br class="">
> Cheers,<br class="">
> Magnus<br class="">
><br class="">
> On 20 December 2016 at 07:48, Magnus Myreen <<a href="mailto:magnus.myreen@gmail.com" class="">magnus.myreen@gmail.com</a>> wrote:<br class="">
>> I don't know if I have any better suggestions. However, I'd like<br class="">
>> everything target specific to live under compiler/targets. The full<br class="">
>> target-specific compilers and configs could be defined in files as<br class="">
>> follows. I'll use x64 as an example:<br class="">
>><br class="">
>> compiler/targets/x64/complete-<wbr class="">compiler/x64_compilerScript.<wbr class="">sml (x64<br class="">
>> config would live here, instantiation of top-level compiler)<br class="">
>> compiler/targets/x64/complete-<wbr class="">compiler/x64_<wbr class="">compilerProofScript.sml<br class="">
>> (proves config_ok and instantiates top-level thm)<br class="">
>> compiler/targets/x64/complete-<wbr class="">compiler/x64_exportLib.sml (provides<br class="">
>> functions for in-logic eval of x64)<br class="">
>><br class="">
>> Note that as much as possible should be shared between all of the<br class="">
>> different targets and be in compiler/. I think generic default<br class="">
>> configurations could be defined in:<br class="">
>><br class="">
>> compiler/configScript.sml<br class="">
>><br class="">
>> There could e.g. be a generic 64-bit config that all 64-bit<br class="">
>> architectures instantiate to their specific config.<br class="">
>><br class="">
>> I think it's a good idea to move the benchmarks to compiler/benchmarks.<br class="">
>><br class="">
>> Cheers,<br class="">
>> Magnus<br class="">
>><br class="">
>> On 20 December 2016 at 06:45, Yong Kiam <<a href="mailto:tanyongkiam@gmail.com" class="">tanyongkiam@gmail.com</a>> wrote:<br class="">
>>> Hi dev,<br class="">
>>><br class="">
>>> I am going to fix up the overloaded eval/ directory. It currently has:<br class="">
>>><br class="">
>>> 1) Definition of the compiler compset<br class="">
>>> 2) Multiple definitions of benchmarks<br class="">
>>> 3) Target configurations, target computeLibs and target exportLibs<br class="">
>>><br class="">
>>> My suggestions:<br class="">
>>><br class="">
>>> 1) Target configurations (configTheory) will go either into compiler/ or<br class="">
>>> compiler/config/. Their proofs will go into a corresponding /proofs<br class="">
>>> directory<br class="">
>>><br class="">
>>> 2) Compiler compset will stay in eval/, the target export and compsets will<br class="">
>>> stay in eval/targets. eval/x64/ will be deleted (it is superceded by the<br class="">
>>> corresponding configuration)<br class="">
>>><br class="">
>>> 3) Benchmarks will move out to compiler/benchmarks and inherit from 2)<br class="">
>>><br class="">
>>> However, there is a bit of a dependency issue: configTheory currently<br class="">
>>> defines the default configuration for every single target in one file. As a<br class="">
>>> result, its heap includes every target.<br class="">
>>><br class="">
>>> The opposite is to follow what's done in targets/ and split everything for<br class="">
>>> each target so that they only inherit the appropriate files. ( This is a bit<br class="">
>>> annoying because there will be a lot of folders with exactly one file in<br class="">
>>> them )<br class="">
>>><br class="">
>>> - targets/{arm,x86, ... }<br class="">
>>> - config/{ arm,x86, ... }<br class="">
>>> - eval/targets/{ ... }<br class="">
>>> - benchmarks/{ ... }<br class="">
>>><br class="">
>>> Does anyone have better suggestions?<br class="">
>>><br class="">
>>> ______________________________<wbr class="">_________________<br class="">
>>> Dev mailing list<br class="">
>>> <a href="mailto:Dev@cakeml.org" class="">Dev@cakeml.org</a><br class="">
>>> <a href="https://lists.cakeml.org/listinfo/dev" rel="noreferrer" target="_blank" class="">https://lists.cakeml.org/<wbr class="">listinfo/dev</a><br class="">
>>><br class="">
><br class="">
> ______________________________<wbr class="">_________________<br class="">
> Dev mailing list<br class="">
> <a href="mailto:Dev@cakeml.org" class="">Dev@cakeml.org</a><br class="">
> <a href="https://lists.cakeml.org/listinfo/dev" rel="noreferrer" target="_blank" class="">https://lists.cakeml.org/<wbr class="">listinfo/dev</a><br class="">
</div></div></blockquote></div><br class=""></div>
_______________________________________________<br class="">Developers mailing list<br class=""><a href="mailto:Developers@cakeml.org" class="">Developers@cakeml.org</a><br class="">https://lists.cakeml.org/listinfo/developers<br class=""></div></blockquote></div><br class=""></body></html>