[CakeML-dev] Re-arranging eval/

Ramana Kumar Ramana.Kumar at cl.cam.ac.uk
Mon Dec 19 22:04:33 UTC 2016

Hi Yong Kiam, developers,

I think this discussion should happen on the Developers list, so I've
changed the CC.

I like Magnus's latest suggestion with regards to the targets/config

I would like the eval directory to be deleted. If we move to
compiler/benchmarks and compiler/x64 etc. then the only thing left in
eval is the compiler compute lib. This, I think, could be split and
left as a single file in various directories, e.g.,
compiler/backend/backendComputeLib.sml, as well as a full merged
version in compiler/compilerComputeLib.sml. Does that sound OK?

I think the directory organisation is rather complex (since there are
a lot of things, and non-trivial dependencies), and it might be
worthwhile sketching a full plan of where we're moving to on the wiki
(e.g., on the Conventions page) to run across all the potential
problems before you start moving files around. It's up to you how you
want to work on it, though :)


On 20 December 2016 at 08:08, Magnus Myreen <magnus.myreen at gmail.com> wrote:
> I take back my previous suggestion regarding compiler/targets, because
> I think the file organisation I suggested is confusing.
> Here's another file organisation:
> compiler/x64
>   is where the instantiation of the top-level compiler to x64 should
> live, including its config, also exportLib for x64
> compiler/x64/proofs
>   a proof of config_ok for x64 and an instantiation of the top-level
> compiler thm
> compiler/x64/encoder  and  compiler/x64/encoder/proofs
>   is what is currently under targets/x64
> The definition of asm and other common infrastructure under
> compiler/targets could move under compiler/backend/asm.
> I suspect this file organisation is more intuitive for people new to
> the code base. If one wants to find the x64 version of the compiler
> one dives into compiler and then into x64, and one finds it. If one
> wants to find the proofs about it, one then dives into proofs and one
> gets to see a short file that opens various important files that one
> can then find my chasing the includes.
> Comments on this suggestion?
> Cheers,
> Magnus
> On 20 December 2016 at 07:48, Magnus Myreen <magnus.myreen at gmail.com> wrote:
>> I don't know if I have any better suggestions. However, I'd like
>> everything target specific to live under compiler/targets. The full
>> target-specific compilers and configs could be defined in files as
>> follows. I'll use x64 as an example:
>>    compiler/targets/x64/complete-compiler/x64_compilerScript.sml  (x64
>> config would live here, instantiation of top-level compiler)
>>    compiler/targets/x64/complete-compiler/x64_compilerProofScript.sml
>> (proves config_ok and instantiates top-level thm)
>>    compiler/targets/x64/complete-compiler/x64_exportLib.sml  (provides
>> functions for in-logic eval of x64)
>> Note that as much as possible should be shared between all of the
>> different targets and be in compiler/. I think generic default
>> configurations could be defined in:
>>   compiler/configScript.sml
>> There could e.g. be a generic 64-bit config that all 64-bit
>> architectures instantiate to their specific config.
>> I think it's a good idea to move the benchmarks to compiler/benchmarks.
>> Cheers,
>> Magnus
>> On 20 December 2016 at 06:45, Yong Kiam <tanyongkiam at gmail.com> wrote:
>>> Hi dev,
>>> I am going to fix up the overloaded eval/ directory. It currently has:
>>> 1) Definition of the compiler compset
>>> 2) Multiple definitions of benchmarks
>>> 3) Target configurations, target computeLibs and target exportLibs
>>> My suggestions:
>>> 1) Target configurations (configTheory) will go either into compiler/ or
>>> compiler/config/. Their proofs will go into a corresponding /proofs
>>> directory
>>> 2) Compiler compset will stay in eval/, the target export and compsets will
>>> stay in eval/targets. eval/x64/ will be deleted (it is superceded by the
>>> corresponding configuration)
>>> 3) Benchmarks will move out to compiler/benchmarks and inherit from 2)
>>> However, there is a bit of a dependency issue: configTheory currently
>>> defines the default configuration for every single target in one file. As a
>>> result, its heap includes every target.
>>> The opposite is to follow what's done in targets/ and split everything for
>>> each target so that they only inherit the appropriate files. ( This is a bit
>>> annoying because there will be a lot of folders with exactly one file in
>>> them )
>>> - targets/{arm,x86, ... }
>>> - config/{ arm,x86, ... }
>>> - eval/targets/{ ... }
>>> - benchmarks/{ ... }
>>> Does anyone have better suggestions?
>>> _______________________________________________
>>> Dev mailing list
>>> Dev at cakeml.org
>>> https://lists.cakeml.org/listinfo/dev
> _______________________________________________
> Dev mailing list
> Dev at cakeml.org
> https://lists.cakeml.org/listinfo/dev

More information about the Developers mailing list