<div dir="ltr"><div>There isn't a way to do the translator for encoders separately yet, but Ramana is working on an abstract translator which should allow it to be translated separately.<br><br></div>The testing sub-directory sounds useful to me too. Maybe the hello-world program could be part of this.<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Dec 22, 2016 at 5:48 AM, Anthony Fox <span dir="ltr"><<a href="mailto:acjf3@cam.ac.uk" target="_blank">acjf3@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 style="word-wrap:break-word"><div>Thanks. Looks fine.</div><div><br></div><div>What’s the situation with regard to regression testing? I know that there are scripts in developers/ for checking the entire system build.</div><div><br></div><div>What I’d like a (relatively) quick way to check if basic encoder dependent stuff is working, i.e.</div><div>• the low-level stages of compilation still evaluate (efficiently)</div><div>• the translator still works (for the encoders)</div><div><br></div><div>Perhaps the bootstrap/ and/or benchmarks/ directories should have a testing/ sub-directory, so as to provide support for quickly sanity checking key parts of the compiler?</div><div><br></div><div>Cheers,</div><div>Anthony</div><div><div class="h5"><br><div><blockquote type="cite"><div>On 21 Dec 2016, at 22:37, Magnus Myreen <<a href="mailto:magnus.myreen@gmail.com" target="_blank">magnus.myreen@gmail.com</a>> wrote:</div><br class="m_3251255264050072000Apple-interchange-newline"><div><div dir="ltr">Hi Anthony,<br><br>We discussed the directory structure at a hangout just now. Yong<br><span id="m_3251255264050072000:1w3.1">Kiam</span>, <span id="m_3251255264050072000:1w3.2">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 id="m_3251255264050072000:1w3.3">https</span>://<span id="m_3251255264050072000:1w3.4">wiki</span>.<span id="m_3251255264050072000:1w3.5">cakeml</span>.org/<wbr>Conventions#directory-<wbr>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 id="m_3251255264050072000:1w3.6">Magnus</span><br><br><br>On 20 December 2016 at 23:27, Anthony Fox <<a href="mailto:acjf3@cam.ac" target="_blank">acjf3@cam.ac</a>.<span id="m_3251255264050072000:1w3.7">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 id="m_3251255264050072000:1w3.8">backend</span><br>> │ ├── <span id="m_3251255264050072000:1w3.9">bignum</span><br>> │ ├── <span id="m_3251255264050072000:1w3.10">gc</span><br>> │ ├── proofs<br>> │ ├── reg_<span id="m_3251255264050072000:1w3.11">alloc</span><br>> │ │ └── proofs<br>> │ └── semantics<br>> ├── bootstrap<br>> │ ├── evaluation<br>> │ ├── <span id="m_3251255264050072000:1w3.12">io</span><br>> │ └── translation<br>> ├── <span id="m_3251255264050072000:1w3.13">eval</span><br>> │ ├── benchmarks<br>> │ │ ├── <span id="m_3251255264050072000:1w3.14">cakeml</span><br>> │ │ ├── <span id="m_3251255264050072000:1w3.15">ocaml</span><br>> │ │ └── poly<br>> │ │ └── other<br>> │ ├── other_benchmarks<br>> │ │ └── <span id="m_3251255264050072000:1w3.16">cakeml</span><br>> │ │ ├── arm<br>> │ │ ├── arm8<br>> │ │ ├── <span id="m_3251255264050072000:1w3.17">mips</span><br>> │ │ ├── <span id="m_3251255264050072000:1w3.18">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 id="m_3251255264050072000:1w3.19">asm</span><br>> ├── <span id="m_3251255264050072000:1w3.20">mips</span><br>> │ └── proofs<br>> ├── <span id="m_3251255264050072000:1w3.21">riscv</span><br>> │ └── proofs<br>> └── x64<br>> └── proofs<br>><br>><br>> On 19 Dec 2016, at 23:46, Yong <span id="m_3251255264050072000:1w3.22">Kiam</span> <<span id="m_3251255264050072000:1w3.23">tanyongkiam</span>@<a href="http://gmail.com/" target="_blank">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 id="m_3251255264050072000:1w3.24">Ramana</span> <span id="m_3251255264050072000:1w3.25">Kumar</span> <<span id="m_3251255264050072000:1w3.26">Ramana</span>.<span id="m_3251255264050072000:1w3.27">Kumar</span>@<a href="http://cl.cam.ac/" target="_blank">cl.cam.ac</a>.<span id="m_3251255264050072000:1w3.28">uk</span>><br>> wrote:<br>>><br>>> Hi Yong <span id="m_3251255264050072000:1w3.29">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 id="m_3251255264050072000:1w3.30">Magnus's</span> latest suggestion with regards to the targets/<span id="m_3251255264050072000:1w3.31">config</span><br>>> organisation.<br>>><br>>> I would like the <span id="m_3251255264050072000:1w3.32">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 id="m_3251255264050072000:1w3.33">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 id="m_3251255264050072000:1w3.34">backend</span>/<span id="m_3251255264050072000:1w3.35">backendComput<wbr>eLib</span>.<span id="m_3251255264050072000:1w3.36">sml</span>, as well as a full merged<br>>> version in compiler/<span id="m_3251255264050072000:1w3.37">compilerComputeLib</span>.<span id="m_3251255264050072000:1w3.38">sm<wbr>l</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 id="m_3251255264050072000:1w3.39">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 id="m_3251255264050072000:1w3.40">Ramana</span><br>>><br>>> On 20 December 2016 at 08:08, <span id="m_3251255264050072000:1w3.41">Magnus</span> <span id="m_3251255264050072000:1w3.42">Myreen</span> <<span id="m_3251255264050072000:1w3.43">magnus</span>.<span id="m_3251255264050072000:1w3.44">myreen</span>@<a href="http://gmail.com/" target="_blank">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 id="m_3251255264050072000:1w3.45">config</span>, also <span id="m_3251255264050072000:1w3.46">exportLib</span> for x64<br>>> ><br>>> > compiler/x64/proofs<br>>> > a proof of <span id="m_3251255264050072000:1w3.47">config</span>_<span id="m_3251255264050072000:1w3.48">ok</span> for x64 and an instantiation of the top-level<br>>> > compiler <span id="m_3251255264050072000:1w3.49">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 id="m_3251255264050072000:1w3.50">asm</span> and other common infrastructure under<br>>> > compiler/targets could move under compiler/<span id="m_3251255264050072000:1w3.51">backend</span>/<span id="m_3251255264050072000:1w3.52">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 id="m_3251255264050072000:1w3.53">Magnus</span><br>>> ><br>>> > On 20 December 2016 at 07:48, <span id="m_3251255264050072000:1w3.54">Magnus</span> <span id="m_3251255264050072000:1w3.55">Myreen</span> <<span id="m_3251255264050072000:1w3.56">magnus</span>.<span id="m_3251255264050072000:1w3.57">myreen</span>@<a href="http://gmail.com/" target="_blank">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 id="m_3251255264050072000:1w3.58">configs</span> could be defined in files as<br>>> >> follows. I'll use x64 as an example:<br>>> >><br>>> >> compiler/targets/x64/<wbr>complete-compiler/x64_<span id="m_3251255264050072000:1w3.59">compiler<wbr>Script</span>.<span id="m_3251255264050072000:1w3.60">sml</span> (x64<br>>> >> <span id="m_3251255264050072000:1w3.61">config</span> would live here, instantiation of top-level compiler)<br>>> >> compiler/targets/x64/<wbr>complete-compiler/x64_<span id="m_3251255264050072000:1w3.62">compiler<wbr>ProofScript</span>.<span id="m_3251255264050072000:1w3.63">sml</span><br>>> >> (proves <span id="m_3251255264050072000:1w3.64">config</span>_<span id="m_3251255264050072000:1w3.65">ok</span> and instantiates top-level <span id="m_3251255264050072000:1w3.66">thm</span>)<br>>> >> compiler/targets/x64/<wbr>complete-compiler/x64_<span id="m_3251255264050072000:1w3.67">exportLi<wbr>b</span>.<span id="m_3251255264050072000:1w3.68">sml</span> (provides<br>>> >> functions for in-logic <span id="m_3251255264050072000:1w3.69">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 id="m_3251255264050072000:1w3.70">configScript</span>.<span id="m_3251255264050072000:1w3.71">sml</span><br>>> >><br>>> >> There could e.g. be a generic 64-bit <span id="m_3251255264050072000:1w3.72">config</span> that all 64-bit<br>>> >> architectures instantiate to their specific <span id="m_3251255264050072000:1w3.73">config</span>.<br>>> >><br>>> >> I think it's a good idea to move the benchmarks to compiler/benchmarks.<br>>> >><br>>> >> Cheers,<br>>> >> <span id="m_3251255264050072000:1w3.74">Magnus</span><br>>> >><br>>> >> On 20 December 2016 at 06:45, Yong <span id="m_3251255264050072000:1w3.75">Kiam</span> <<span id="m_3251255264050072000:1w3.76">tanyongkiam</span>@<a href="http://gmail.com/" target="_blank">gmail.com</a>> wrote:<br>>> >>> Hi <span id="m_3251255264050072000:1w3.77">dev</span>,<br>>> >>><br>>> >>> I am going to fix up the overloaded <span id="m_3251255264050072000:1w3.78">eval</span>/ directory. It currently has:<br>>> >>><br>>> >>> 1) Definition of the compiler <span id="m_3251255264050072000:1w3.79">compset</span><br>>> >>> 2) Multiple definitions of benchmarks<br>>> >>> 3) Target configurations, target <span id="m_3251255264050072000:1w3.80">computeLibs</span> and target <span id="m_3251255264050072000:1w3.81">exportLibs</span><br>>> >>><br>>> >>> My suggestions:<br>>> >>><br>>> >>> 1) Target configurations (<span id="m_3251255264050072000:1w3.82">configTheory</span>) will go either into compiler/<br>>> >>> or<br>>> >>> compiler/<span id="m_3251255264050072000:1w3.83">config</span>/. Their proofs will go into a corresponding /proofs<br>>> >>> directory<br>>> >>><br>>> >>> 2) Compiler <span id="m_3251255264050072000:1w3.84">compset</span> will stay in <span id="m_3251255264050072000:1w3.85">eval</span>/, the target export and <span id="m_3251255264050072000:1w3.86">compsets</span><br>>> >>> will<br>>> >>> stay in <span id="m_3251255264050072000:1w3.87">eval</span>/targets. <span id="m_3251255264050072000:1w3.88">eval</span>/x64/ will be deleted (it is <span id="m_3251255264050072000:1w3.89">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 id="m_3251255264050072000:1w3.90">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 id="m_3251255264050072000:1w3.101">config</span>/{ arm,x86, ... }<br>>> >>> - <span id="m_3251255264050072000:1w3.103">eval</span>/targets/{ ... }<br>>> >>> - benchmarks/{ ... }<br>>> >>><br>>> >>> Does anyone have better suggestions?<br>>> >>><br>>> >>> ______________________________<wbr>_________________<br>>> >>> Dev mailing list<br>>> >>> Dev@<span id="m_3251255264050072000:1w3.107">cakeml</span>.org<br>>> >>> <span id="m_3251255264050072000:1w3.108">https</span>://lists.<span id="m_3251255264050072000:1w3.110">cakeml</span>.org/<span id="m_3251255264050072000:1w3.111">listi<wbr>nfo</span>/<span id="m_3251255264050072000:1w3.112">dev</span><br>>> >>><br>>> ><br>>> > ______________________________<wbr>_________________<br>>> > Dev mailing list<br>>> > Dev@<span id="m_3251255264050072000:1w3.116">cakeml</span>.org<br>>> > <span id="m_3251255264050072000:1w3.117">https</span>://lists.<span id="m_3251255264050072000:1w3.119">cakeml</span>.org/<span id="m_3251255264050072000:1w3.120">listi<wbr>nfo</span>/<span id="m_3251255264050072000:1w3.121">dev</span><br>><br>><br>> ______________________________<wbr>_________________<br>> Developers mailing list<br>> Developers@<span id="m_3251255264050072000:1w3.123">cakeml</span>.org<br>> <span id="m_3251255264050072000:1w3.124">https</span>://lists.<span id="m_3251255264050072000:1w3.126">cakeml</span>.org/<span id="m_3251255264050072000:1w3.127">listi<wbr>nfo</span>/developers<br>><br>></div></div>
</div></blockquote></div><br></div></div></div></blockquote></div><br></div>