[CakeML-dev] Re-arranging eval/
Magnus Myreen
magnus.myreen at gmail.com
Wed Dec 21 22:37:10 UTC 2016
Hi Anthony,
We discussed the directory structure at a hangout just now. Yong
Kiam, Ramana and I (the only ones at the hangout) sketched a goal for
the reorganisation based on your depiction of the current directory
structure.
https://wiki.cakeml.org/Conventions#directory-structure
Regarding targets directory, we essentially just renamed the directory
to encoders, and renamed targets/all to encoders/testing. Feel free to
make edits to the plan.
The reorganisation won't happen immediately.
Cheers,
Magnus
On 20 December 2016 at 23:27, Anthony Fox <acjf3 at cam.ac.uk> wrote:
> Thought it may be helpful to show the current directory structure
(below). I
> have a preference for compiler/targets/x64 over compiler/x64, especially
if
> the new targets/ directory did actually contain all of the target specific
> stuff. - Anthony
>
> .
> ├── backend
> │ ├── bignum
> │ ├── gc
> │ ├── proofs
> │ ├── reg_alloc
> │ │ └── proofs
> │ └── semantics
> ├── bootstrap
> │ ├── evaluation
> │ ├── io
> │ └── translation
> ├── eval
> │ ├── benchmarks
> │ │ ├── cakeml
> │ │ ├── ocaml
> │ │ └── poly
> │ │ └── other
> │ ├── other_benchmarks
> │ │ └── cakeml
> │ │ ├── arm
> │ │ ├── arm8
> │ │ ├── mips
> │ │ ├── riscv
> │ │ └── x64
> │ ├── targets
> │ │ └── proofs
> │ └── x64
> ├── inference
> │ └── proofs
> ├── parsing
> │ ├── proofs
> │ └── testing
> ├── proofs
> └── targets
> ├── all
> ├── arm6
> │ └── proofs
> ├── arm8
> │ └── proofs
> ├── asm
> ├── mips
> │ └── proofs
> ├── riscv
> │ └── proofs
> └── x64
> └── proofs
>
>
> On 19 Dec 2016, at 23:46, Yong Kiam <tanyongkiam at gmail.com> wrote:
>
> 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.
>
> On Mon, Dec 19, 2016 at 5:04 PM, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>
> wrote:
>>
>> 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
>> organisation.
>>
>> 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 :)
>>
>> Cheers,
>> Ramana
>>
>> 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
>
>
> _______________________________________________
> Developers mailing list
> Developers at cakeml.org
> https://lists.cakeml.org/listinfo/developers
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20161222/2041e38b/attachment-0001.html>
More information about the Developers
mailing list