<div dir="ltr">Hi Anthony,<br><br>We discussed the directory structure at a hangout just now. Yong<br><span class="" id=":1w3.1" tabindex="-1">Kiam</span>, <span class="" id=":1w3.2" tabindex="-1">Ramana</span> and I (the only ones at the hangout) sketched a goal for<br>the reorganisation based on your depiction of the current directory <div>structure.<br><br><span class="" id=":1w3.3" tabindex="-1">https</span>://<span class="" id=":1w3.4" tabindex="-1">wiki</span>.<span class="" id=":1w3.5" tabindex="-1">cakeml</span>.org/Conventions#directory-structure<br> </div><div>Regarding targets directory, we essentially just renamed the directory </div><div>to encoders, and renamed targets/all to encoders/testing. Feel free to </div><div>make edits to the plan.<br><br>The reorganisation won't happen immediately.<br><br>Cheers,<br><span class="" id=":1w3.6" tabindex="-1">Magnus</span><br><br><br>On 20 December 2016 at 23:27, Anthony Fox <<a href="mailto:acjf3@cam.ac">acjf3@cam.ac</a>.<span class="" id=":1w3.7" tabindex="-1">uk</span>> wrote:<br>> Thought it may be helpful to show the current directory structure (below). I<br>> have a preference for compiler/targets/x64 over compiler/x64, especially if<br>> the new targets/ directory did actually contain all of the target specific<br>> stuff. - Anthony<br>><br>> .<br>> ├── <span class="" id=":1w3.8" tabindex="-1">backend</span><br>> │   ├── <span class="" id=":1w3.9" tabindex="-1">bignum</span><br>> │   ├── <span class="" id=":1w3.10" tabindex="-1">gc</span><br>> │   ├── proofs<br>> │   ├── reg_<span class="" id=":1w3.11" tabindex="-1">alloc</span><br>> │   │   └── proofs<br>> │   └── semantics<br>> ├── bootstrap<br>> │   ├── evaluation<br>> │   ├── <span class="" id=":1w3.12" tabindex="-1">io</span><br>> │   └── translation<br>> ├── <span class="" id=":1w3.13" tabindex="-1">eval</span><br>> │   ├── benchmarks<br>> │   │   ├── <span class="" id=":1w3.14" tabindex="-1">cakeml</span><br>> │   │   ├── <span class="" id=":1w3.15" tabindex="-1">ocaml</span><br>> │   │   └── poly<br>> │   │       └── other<br>> │   ├── other_benchmarks<br>> │   │   └── <span class="" id=":1w3.16" tabindex="-1">cakeml</span><br>> │   │       ├── arm<br>> │   │       ├── arm8<br>> │   │       ├── <span class="" id=":1w3.17" tabindex="-1">mips</span><br>> │   │       ├── <span class="" id=":1w3.18" tabindex="-1">riscv</span><br>> │   │       └── x64<br>> │   ├── targets<br>> │   │   └── proofs<br>> │   └── x64<br>> ├── inference<br>> │   └── proofs<br>> ├── parsing<br>> │   ├── proofs<br>> │   └── testing<br>> ├── proofs<br>> └── targets<br>>     ├── all<br>>     ├── arm6<br>>     │   └── proofs<br>>     ├── arm8<br>>     │   └── proofs<br>>     ├── <span class="" id=":1w3.19" tabindex="-1">asm</span><br>>     ├── <span class="" id=":1w3.20" tabindex="-1">mips</span><br>>     │   └── proofs<br>>     ├── <span class="" id=":1w3.21" tabindex="-1">riscv</span><br>>     │   └── proofs<br>>     └── x64<br>>         └── proofs<br>><br>><br>> On 19 Dec 2016, at 23:46, Yong <span class="" id=":1w3.22" tabindex="-1">Kiam</span> <<span class="" id=":1w3.23" tabindex="-1">tanyongkiam</span>@<a href="http://gmail.com">gmail.com</a>> wrote:<br>><br>> Your plan combined with Magnus' sound good. We could finalise the sketching<br>> at the next hangout in case anyone has other suggestions, or has things to<br>> point out.<br>><br>> On Mon, Dec 19, 2016 at 5:04 PM, <span class="" id=":1w3.24" tabindex="-1">Ramana</span> <span class="" id=":1w3.25" tabindex="-1">Kumar</span> <<span class="" id=":1w3.26" tabindex="-1">Ramana</span>.<span class="" id=":1w3.27" tabindex="-1">Kumar</span>@<a href="http://cl.cam.ac">cl.cam.ac</a>.<span class="" id=":1w3.28" tabindex="-1">uk</span>><br>> wrote:<br>>><br>>> Hi Yong <span class="" id=":1w3.29" tabindex="-1">Kiam</span>, developers,<br>>><br>>> I think this discussion should happen on the Developers list, so I've<br>>> changed the CC.<br>>><br>>> I like <span class="" id=":1w3.30" tabindex="-1">Magnus's</span> latest suggestion with regards to the targets/<span class="" id=":1w3.31" tabindex="-1">config</span><br>>> organisation.<br>>><br>>> I would like the <span class="" id=":1w3.32" tabindex="-1">eval</span> directory to be deleted. If we move to<br>>> compiler/benchmarks and compiler/x64 etc. then the only thing left in<br>>> <span class="" id=":1w3.33" tabindex="-1">eval</span> 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/<span class="" id=":1w3.34" tabindex="-1">backend</span>/<span class="" id=":1w3.35" tabindex="-1">backendComputeLib</span>.<span class="" id=":1w3.36" tabindex="-1">sml</span>, as well as a full merged<br>>> version in compiler/<span class="" id=":1w3.37" tabindex="-1">compilerComputeLib</span>.<span class="" id=":1w3.38" tabindex="-1">sml</span>. 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 <span class="" id=":1w3.39" tabindex="-1">wiki</span><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>>> <span class="" id=":1w3.40" tabindex="-1">Ramana</span><br>>><br>>> On 20 December 2016 at 08:08, <span class="" id=":1w3.41" tabindex="-1">Magnus</span> <span class="" id=":1w3.42" tabindex="-1">Myreen</span> <<span class="" id=":1w3.43" tabindex="-1">magnus</span>.<span class="" id=":1w3.44" tabindex="-1">myreen</span>@<a href="http://gmail.com">gmail.com</a>><br>>> 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 <span class="" id=":1w3.45" tabindex="-1">config</span>, also <span class="" id=":1w3.46" tabindex="-1">exportLib</span> for x64<br>>> ><br>>> > compiler/x64/proofs<br>>> >   a proof of <span class="" id=":1w3.47" tabindex="-1">config</span>_<span class="" id=":1w3.48" tabindex="-1">ok</span> for x64 and an instantiation of the top-level<br>>> > compiler <span class="" id=":1w3.49" tabindex="-1">thm</span><br>>> ><br>>> > compiler/x64/encoder  and  compiler/x64/encoder/proofs<br>>> >   is what is currently under targets/x64<br>>> ><br>>> > The definition of <span class="" id=":1w3.50" tabindex="-1">asm</span> and other common infrastructure under<br>>> > compiler/targets could move under compiler/<span class="" id=":1w3.51" tabindex="-1">backend</span>/<span class="" id=":1w3.52" tabindex="-1">asm</span>.<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>>> > <span class="" id=":1w3.53" tabindex="-1">Magnus</span><br>>> ><br>>> > On 20 December 2016 at 07:48, <span class="" id=":1w3.54" tabindex="-1">Magnus</span> <span class="" id=":1w3.55" tabindex="-1">Myreen</span> <<span class="" id=":1w3.56" tabindex="-1">magnus</span>.<span class="" id=":1w3.57" tabindex="-1">myreen</span>@<a href="http://gmail.com">gmail.com</a>><br>>> > 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 <span class="" id=":1w3.58" tabindex="-1">configs</span> could be defined in files as<br>>> >> follows. I'll use x64 as an example:<br>>> >><br>>> >>    compiler/targets/x64/complete-compiler/x64_<span class="" id=":1w3.59" tabindex="-1">compilerScript</span>.<span class="" id=":1w3.60" tabindex="-1">sml</span>  (x64<br>>> >> <span class="" id=":1w3.61" tabindex="-1">config</span> would live here, instantiation of top-level compiler)<br>>> >>    compiler/targets/x64/complete-compiler/x64_<span class="" id=":1w3.62" tabindex="-1">compilerProofScript</span>.<span class="" id=":1w3.63" tabindex="-1">sml</span><br>>> >> (proves <span class="" id=":1w3.64" tabindex="-1">config</span>_<span class="" id=":1w3.65" tabindex="-1">ok</span> and instantiates top-level <span class="" id=":1w3.66" tabindex="-1">thm</span>)<br>>> >>    compiler/targets/x64/complete-compiler/x64_<span class="" id=":1w3.67" tabindex="-1">exportLib</span>.<span class="" id=":1w3.68" tabindex="-1">sml</span>  (provides<br>>> >> functions for in-logic <span class="" id=":1w3.69" tabindex="-1">eval</span> 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/<span class="" id=":1w3.70" tabindex="-1">configScript</span>.<span class="" id=":1w3.71" tabindex="-1">sml</span><br>>> >><br>>> >> There could e.g. be a generic 64-bit <span class="" id=":1w3.72" tabindex="-1">config</span> that all 64-bit<br>>> >> architectures instantiate to their specific <span class="" id=":1w3.73" tabindex="-1">config</span>.<br>>> >><br>>> >> I think it's a good idea to move the benchmarks to compiler/benchmarks.<br>>> >><br>>> >> Cheers,<br>>> >> <span class="" id=":1w3.74" tabindex="-1">Magnus</span><br>>> >><br>>> >> On 20 December 2016 at 06:45, Yong <span class="" id=":1w3.75" tabindex="-1">Kiam</span> <<span class="" id=":1w3.76" tabindex="-1">tanyongkiam</span>@<a href="http://gmail.com">gmail.com</a>> wrote:<br>>> >>> Hi <span class="" id=":1w3.77" tabindex="-1">dev</span>,<br>>> >>><br>>> >>> I am going to fix up the overloaded <span class="" id=":1w3.78" tabindex="-1">eval</span>/ directory. It currently has:<br>>> >>><br>>> >>> 1) Definition of the compiler <span class="" id=":1w3.79" tabindex="-1">compset</span><br>>> >>> 2) Multiple definitions of benchmarks<br>>> >>> 3) Target configurations, target <span class="" id=":1w3.80" tabindex="-1">computeLibs</span> and target <span class="" id=":1w3.81" tabindex="-1">exportLibs</span><br>>> >>><br>>> >>> My suggestions:<br>>> >>><br>>> >>> 1) Target configurations (<span class="" id=":1w3.82" tabindex="-1">configTheory</span>) will go either into compiler/<br>>> >>> or<br>>> >>> compiler/<span class="" id=":1w3.83" tabindex="-1">config</span>/. Their proofs will go into a corresponding /proofs<br>>> >>> directory<br>>> >>><br>>> >>> 2) Compiler <span class="" id=":1w3.84" tabindex="-1">compset</span> will stay in <span class="" id=":1w3.85" tabindex="-1">eval</span>/, the target export and <span class="" id=":1w3.86" tabindex="-1">compsets</span><br>>> >>> will<br>>> >>> stay in <span class="" id=":1w3.87" tabindex="-1">eval</span>/targets. <span class="" id=":1w3.88" tabindex="-1">eval</span>/x64/ will be deleted (it is <span class="" id=":1w3.89" tabindex="-1">superceded</span> by<br>>> >>> 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: <span class="" id=":1w3.90" tabindex="-1">configTheory</span> currently<br>>> >>> defines the default configuration for every single target in one file.<br>>> >>> As a<br>>> >>> result, its heap includes every target.<br>>> >>><br>>> >>> The opposite is to follow what's done in targets/ and split everything<br>>> >>> for<br>>> >>> each target so that they only inherit the appropriate files. ( This is<br>>> >>> a bit<br>>> >>> annoying because there will be a lot of folders with exactly one file<br>>> >>> in<br>>> >>> them )<br>>> >>><br>>> >>> - targets/{arm,x86, ... }<br>>> >>> - <span class="" id=":1w3.101" tabindex="-1">config</span>/{ arm,x86, ... }<br>>> >>> - <span class="" id=":1w3.103" tabindex="-1">eval</span>/targets/{ ... }<br>>> >>> - benchmarks/{ ... }<br>>> >>><br>>> >>> Does anyone have better suggestions?<br>>> >>><br>>> >>> _______________________________________________<br>>> >>> Dev mailing list<br>>> >>> Dev@<span class="" id=":1w3.107" tabindex="-1">cakeml</span>.org<br>>> >>> <span class="" id=":1w3.108" tabindex="-1">https</span>://lists.<span class="" id=":1w3.110" tabindex="-1">cakeml</span>.org/<span class="" id=":1w3.111" tabindex="-1">listinfo</span>/<span class="" id=":1w3.112" tabindex="-1">dev</span><br>>> >>><br>>> ><br>>> > _______________________________________________<br>>> > Dev mailing list<br>>> > Dev@<span class="" id=":1w3.116" tabindex="-1">cakeml</span>.org<br>>> > <span class="" id=":1w3.117" tabindex="-1">https</span>://lists.<span class="" id=":1w3.119" tabindex="-1">cakeml</span>.org/<span class="" id=":1w3.120" tabindex="-1">listinfo</span>/<span class="" id=":1w3.121" tabindex="-1">dev</span><br>><br>><br>> _______________________________________________<br>> Developers mailing list<br>> Developers@<span class="" id=":1w3.123" tabindex="-1">cakeml</span>.org<br>> <span class="" id=":1w3.124" tabindex="-1">https</span>://lists.<span class="" id=":1w3.126" tabindex="-1">cakeml</span>.org/<span class="" id=":1w3.127" tabindex="-1">listinfo</span>/developers<br>><br>></div></div>