<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="">Thanks. Looks fine.</div><div class=""><br class=""></div><div class="">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 class=""><br class=""></div><div class="">What I’d like a (relatively) quick way to check if basic encoder dependent stuff is working, i.e.</div><div class="">• the low-level stages of compilation still evaluate (efficiently)</div><div class="">• the translator still works (for the encoders)</div><div class=""><br class=""></div><div class="">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 class=""><br class=""></div><div class="">Cheers,</div><div class="">Anthony</div><br class=""><div><blockquote type="cite" class=""><div class="">On 21 Dec 2016, at 22:37, Magnus Myreen <<a href="mailto:magnus.myreen@gmail.com" class="">magnus.myreen@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class="">Hi Anthony,<br class=""><br class="">We discussed the directory structure at a hangout just now. Yong<br class=""><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 class="">the reorganisation based on your depiction of the current directory <div class="">structure.<br class=""><br class=""><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 class=""> </div><div class="">Regarding targets directory, we essentially just renamed the directory </div><div class="">to encoders, and renamed targets/all to encoders/testing. Feel free to </div><div class="">make edits to the plan.<br class=""><br class="">The reorganisation won't happen immediately.<br class=""><br class="">Cheers,<br class=""><span class="" id=":1w3.6" tabindex="-1">Magnus</span><br class=""><br class=""><br class="">On 20 December 2016 at 23:27, Anthony Fox <<a href="mailto:acjf3@cam.ac" class="">acjf3@cam.ac</a>.<span class="" id=":1w3.7" tabindex="-1">uk</span>> wrote:<br class="">> Thought it may be helpful to show the current directory structure (below). I<br class="">> have a preference for compiler/targets/x64 over compiler/x64, especially if<br class="">> the new targets/ directory did actually contain all of the target specific<br class="">> stuff. - Anthony<br class="">><br class="">> .<br class="">> ├── <span class="" id=":1w3.8" tabindex="-1">backend</span><br class="">> │ ├── <span class="" id=":1w3.9" tabindex="-1">bignum</span><br class="">> │ ├── <span class="" id=":1w3.10" tabindex="-1">gc</span><br class="">> │ ├── proofs<br class="">> │ ├── reg_<span class="" id=":1w3.11" tabindex="-1">alloc</span><br class="">> │ │ └── proofs<br class="">> │ └── semantics<br class="">> ├── bootstrap<br class="">> │ ├── evaluation<br class="">> │ ├── <span class="" id=":1w3.12" tabindex="-1">io</span><br class="">> │ └── translation<br class="">> ├── <span class="" id=":1w3.13" tabindex="-1">eval</span><br class="">> │ ├── benchmarks<br class="">> │ │ ├── <span class="" id=":1w3.14" tabindex="-1">cakeml</span><br class="">> │ │ ├── <span class="" id=":1w3.15" tabindex="-1">ocaml</span><br class="">> │ │ └── poly<br class="">> │ │ └── other<br class="">> │ ├── other_benchmarks<br class="">> │ │ └── <span class="" id=":1w3.16" tabindex="-1">cakeml</span><br class="">> │ │ ├── arm<br class="">> │ │ ├── arm8<br class="">> │ │ ├── <span class="" id=":1w3.17" tabindex="-1">mips</span><br class="">> │ │ ├── <span class="" id=":1w3.18" tabindex="-1">riscv</span><br class="">> │ │ └── x64<br class="">> │ ├── targets<br class="">> │ │ └── proofs<br class="">> │ └── x64<br class="">> ├── inference<br class="">> │ └── proofs<br class="">> ├── parsing<br class="">> │ ├── proofs<br class="">> │ └── testing<br class="">> ├── proofs<br class="">> └── targets<br class="">> ├── all<br class="">> ├── arm6<br class="">> │ └── proofs<br class="">> ├── arm8<br class="">> │ └── proofs<br class="">> ├── <span class="" id=":1w3.19" tabindex="-1">asm</span><br class="">> ├── <span class="" id=":1w3.20" tabindex="-1">mips</span><br class="">> │ └── proofs<br class="">> ├── <span class="" id=":1w3.21" tabindex="-1">riscv</span><br class="">> │ └── proofs<br class="">> └── x64<br class="">> └── proofs<br class="">><br class="">><br class="">> 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/" class="">gmail.com</a>> wrote:<br class="">><br class="">> Your plan combined with Magnus' sound good. We could finalise the sketching<br class="">> at the next hangout in case anyone has other suggestions, or has things to<br class="">> point out.<br class="">><br class="">> 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/" class="">cl.cam.ac</a>.<span class="" id=":1w3.28" tabindex="-1">uk</span>><br class="">> wrote:<br class="">>><br class="">>> Hi Yong <span class="" id=":1w3.29" tabindex="-1">Kiam</span>, 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 <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 class="">>> organisation.<br class="">>><br class="">>> I would like the <span class="" id=":1w3.32" tabindex="-1">eval</span> directory to be deleted. If we move to<br class="">>> compiler/benchmarks and compiler/x64 etc. then the only thing left in<br class="">>> <span class="" id=":1w3.33" tabindex="-1">eval</span> 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/<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 class="">>> 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 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 <span class="" id=":1w3.39" tabindex="-1">wiki</span><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="">>> <span class="" id=":1w3.40" tabindex="-1">Ramana</span><br class="">>><br class="">>> 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/" class="">gmail.com</a>><br class="">>> 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 <span class="" id=":1w3.45" tabindex="-1">config</span>, also <span class="" id=":1w3.46" tabindex="-1">exportLib</span> for x64<br class="">>> ><br class="">>> > compiler/x64/proofs<br class="">>> > 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 class="">>> > compiler <span class="" id=":1w3.49" tabindex="-1">thm</span><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 <span class="" id=":1w3.50" tabindex="-1">asm</span> and other common infrastructure under<br class="">>> > 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 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="">>> > <span class="" id=":1w3.53" tabindex="-1">Magnus</span><br class="">>> ><br class="">>> > 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/" class="">gmail.com</a>><br class="">>> > 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 <span class="" id=":1w3.58" tabindex="-1">configs</span> could be defined in files as<br class="">>> >> follows. I'll use x64 as an example:<br class="">>> >><br class="">>> >> 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 class="">>> >> <span class="" id=":1w3.61" tabindex="-1">config</span> would live here, instantiation of top-level compiler)<br class="">>> >> 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 class="">>> >> (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 class="">>> >> 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 class="">>> >> functions for in-logic <span class="" id=":1w3.69" tabindex="-1">eval</span> 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/<span class="" id=":1w3.70" tabindex="-1">configScript</span>.<span class="" id=":1w3.71" tabindex="-1">sml</span><br class="">>> >><br class="">>> >> There could e.g. be a generic 64-bit <span class="" id=":1w3.72" tabindex="-1">config</span> that all 64-bit<br class="">>> >> architectures instantiate to their specific <span class="" id=":1w3.73" tabindex="-1">config</span>.<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="">>> >> <span class="" id=":1w3.74" tabindex="-1">Magnus</span><br class="">>> >><br class="">>> >> 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/" class="">gmail.com</a>> wrote:<br class="">>> >>> Hi <span class="" id=":1w3.77" tabindex="-1">dev</span>,<br class="">>> >>><br class="">>> >>> I am going to fix up the overloaded <span class="" id=":1w3.78" tabindex="-1">eval</span>/ directory. It currently has:<br class="">>> >>><br class="">>> >>> 1) Definition of the compiler <span class="" id=":1w3.79" tabindex="-1">compset</span><br class="">>> >>> 2) Multiple definitions of benchmarks<br class="">>> >>> 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 class="">>> >>><br class="">>> >>> My suggestions:<br class="">>> >>><br class="">>> >>> 1) Target configurations (<span class="" id=":1w3.82" tabindex="-1">configTheory</span>) will go either into compiler/<br class="">>> >>> or<br class="">>> >>> compiler/<span class="" id=":1w3.83" tabindex="-1">config</span>/. Their proofs will go into a corresponding /proofs<br class="">>> >>> directory<br class="">>> >>><br class="">>> >>> 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 class="">>> >>> will<br class="">>> >>> 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 class="">>> >>> 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: <span class="" id=":1w3.90" tabindex="-1">configTheory</span> currently<br class="">>> >>> defines the default configuration for every single target in one file.<br class="">>> >>> 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<br class="">>> >>> for<br class="">>> >>> each target so that they only inherit the appropriate files. ( This is<br class="">>> >>> a bit<br class="">>> >>> annoying because there will be a lot of folders with exactly one file<br class="">>> >>> in<br class="">>> >>> them )<br class="">>> >>><br class="">>> >>> - targets/{arm,x86, ... }<br class="">>> >>> - <span class="" id=":1w3.101" tabindex="-1">config</span>/{ arm,x86, ... }<br class="">>> >>> - <span class="" id=":1w3.103" tabindex="-1">eval</span>/targets/{ ... }<br class="">>> >>> - benchmarks/{ ... }<br class="">>> >>><br class="">>> >>> Does anyone have better suggestions?<br class="">>> >>><br class="">>> >>> _______________________________________________<br class="">>> >>> Dev mailing list<br class="">>> >>> Dev@<span class="" id=":1w3.107" tabindex="-1">cakeml</span>.org<br class="">>> >>> <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 class="">>> >>><br class="">>> ><br class="">>> > _______________________________________________<br class="">>> > Dev mailing list<br class="">>> > Dev@<span class="" id=":1w3.116" tabindex="-1">cakeml</span>.org<br class="">>> > <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 class="">><br class="">><br class="">> _______________________________________________<br class="">> Developers mailing list<br class="">> Developers@<span class="" id=":1w3.123" tabindex="-1">cakeml</span>.org<br class="">> <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 class="">><br class="">></div></div>
</div></blockquote></div><br class=""></body></html>