<div dir="ltr">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></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Dec 19, 2016 at 5:04 PM, 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">Hi Yong Kiam, developers,<br>
<br>
I think this discussion should happen on the Developers list, so I've<br>
changed the CC.<br>
<br>
I like Magnus's latest suggestion with regards to the targets/config<br>
organisation.<br>
<br>
I would like the eval directory to be deleted. If we move to<br>
compiler/benchmarks and compiler/x64 etc. then the only thing left in<br>
eval is the compiler compute lib. This, I think, could be split and<br>
left as a single file in various directories, e.g.,<br>
compiler/backend/<wbr>backendComputeLib.sml, as well as a full merged<br>
version in compiler/compilerComputeLib.<wbr>sml. Does that sound OK?<br>
<br>
I think the directory organisation is rather complex (since there are<br>
a lot of things, and non-trivial dependencies), and it might be<br>
worthwhile sketching a full plan of where we're moving to on the wiki<br>
(e.g., on the Conventions page) to run across all the potential<br>
problems before you start moving files around. It's up to you how you<br>
want to work on it, though :)<br>
<br>
Cheers,<br>
Ramana<br>
<div class="HOEnZb"><div class="h5"><br>
On 20 December 2016 at 08:08, Magnus Myreen <<a href="mailto:magnus.myreen@gmail.com">magnus.myreen@gmail.com</a>> wrote:<br>
> I take back my previous suggestion regarding compiler/targets, because<br>
> I think the file organisation I suggested is confusing.<br>
><br>
> Here's another file organisation:<br>
><br>
> compiler/x64<br>
>   is where the instantiation of the top-level compiler to x64 should<br>
> live, including its config, also exportLib for x64<br>
><br>
> compiler/x64/proofs<br>
>   a proof of config_ok for x64 and an instantiation of the top-level<br>
> compiler thm<br>
><br>
> compiler/x64/encoder  and  compiler/x64/encoder/proofs<br>
>   is what is currently under targets/x64<br>
><br>
> The definition of asm and other common infrastructure under<br>
> compiler/targets could move under compiler/backend/asm.<br>
><br>
> I suspect this file organisation is more intuitive for people new to<br>
> the code base. If one wants to find the x64 version of the compiler<br>
> one dives into compiler and then into x64, and one finds it. If one<br>
> wants to find the proofs about it, one then dives into proofs and one<br>
> gets to see a short file that opens various important files that one<br>
> can then find my chasing the includes.<br>
><br>
> Comments on this suggestion?<br>
><br>
> Cheers,<br>
> Magnus<br>
><br>
> On 20 December 2016 at 07:48, Magnus Myreen <<a href="mailto:magnus.myreen@gmail.com">magnus.myreen@gmail.com</a>> wrote:<br>
>> I don't know if I have any better suggestions. However, I'd like<br>
>> everything target specific to live under compiler/targets. The full<br>
>> target-specific compilers and configs could be defined in files as<br>
>> follows. I'll use x64 as an example:<br>
>><br>
>>    compiler/targets/x64/complete-<wbr>compiler/x64_compilerScript.<wbr>sml  (x64<br>
>> config would live here, instantiation of top-level compiler)<br>
>>    compiler/targets/x64/complete-<wbr>compiler/x64_<wbr>compilerProofScript.sml<br>
>> (proves config_ok and instantiates top-level thm)<br>
>>    compiler/targets/x64/complete-<wbr>compiler/x64_exportLib.sml  (provides<br>
>> functions for in-logic eval of x64)<br>
>><br>
>> Note that as much as possible should be shared between all of the<br>
>> different targets and be in compiler/. I think generic default<br>
>> configurations could be defined in:<br>
>><br>
>>   compiler/configScript.sml<br>
>><br>
>> There could e.g. be a generic 64-bit config that all 64-bit<br>
>> architectures instantiate to their specific config.<br>
>><br>
>> I think it's a good idea to move the benchmarks to compiler/benchmarks.<br>
>><br>
>> Cheers,<br>
>> Magnus<br>
>><br>
>> On 20 December 2016 at 06:45, Yong Kiam <<a href="mailto:tanyongkiam@gmail.com">tanyongkiam@gmail.com</a>> wrote:<br>
>>> Hi dev,<br>
>>><br>
>>> I am going to fix up the overloaded eval/ directory. It currently has:<br>
>>><br>
>>> 1) Definition of the compiler compset<br>
>>> 2) Multiple definitions of benchmarks<br>
>>> 3) Target configurations, target computeLibs and target exportLibs<br>
>>><br>
>>> My suggestions:<br>
>>><br>
>>> 1) Target configurations (configTheory) will go either into compiler/ or<br>
>>> compiler/config/. Their proofs will go into a corresponding /proofs<br>
>>> directory<br>
>>><br>
>>> 2) Compiler compset will stay in eval/, the target export and compsets will<br>
>>> stay in eval/targets. eval/x64/ will be deleted (it is superceded by the<br>
>>> corresponding configuration)<br>
>>><br>
>>> 3) Benchmarks will move out to compiler/benchmarks and inherit from 2)<br>
>>><br>
>>> However, there is a bit of a dependency issue: configTheory currently<br>
>>> defines the default configuration for every single target in one file. As a<br>
>>> result, its heap includes every target.<br>
>>><br>
>>> The opposite is to follow what's done in targets/ and split everything for<br>
>>> each target so that they only inherit the appropriate files. ( This is a bit<br>
>>> annoying because there will be a lot of folders with exactly one file in<br>
>>> them )<br>
>>><br>
>>> - targets/{arm,x86, ... }<br>
>>> - config/{ arm,x86, ... }<br>
>>> - eval/targets/{ ... }<br>
>>> - benchmarks/{ ... }<br>
>>><br>
>>> Does anyone have better suggestions?<br>
>>><br>
>>> ______________________________<wbr>_________________<br>
>>> Dev mailing list<br>
>>> <a href="mailto:Dev@cakeml.org">Dev@cakeml.org</a><br>
>>> <a href="https://lists.cakeml.org/listinfo/dev" rel="noreferrer" target="_blank">https://lists.cakeml.org/<wbr>listinfo/dev</a><br>
>>><br>
><br>
> ______________________________<wbr>_________________<br>
> Dev mailing list<br>
> <a href="mailto:Dev@cakeml.org">Dev@cakeml.org</a><br>
> <a href="https://lists.cakeml.org/listinfo/dev" rel="noreferrer" target="_blank">https://lists.cakeml.org/<wbr>listinfo/dev</a><br>
</div></div></blockquote></div><br></div>