[CakeML-dev] Re-arranging eval/

Anthony Fox acjf3 at cam.ac.uk
Tue Dec 20 12:27:03 UTC 2016 

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 <mailto: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 <mailto: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 <mailto: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 <mailto: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 <mailto:Dev at cakeml.org>
> >>> https://lists.cakeml.org/listinfo/dev <https://lists.cakeml.org/listinfo/dev>
> >>>
> >
> > _______________________________________________
> > Dev mailing list
> > Dev at cakeml.org <mailto:Dev at cakeml.org>
> > https://lists.cakeml.org/listinfo/dev <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/20161220/c09525b6/attachment-0001.html>

More information about the Developers mailing list