[CakeML-dev] Re-arranging eval/

Yong Kiam tanyongkiam at gmail.com
Fri Dec 23 16:28:41 UTC 2016


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.

The testing sub-directory sounds useful to me too. Maybe the hello-world
program could be part of this.

On Thu, Dec 22, 2016 at 5:48 AM, Anthony Fox <acjf3 at cam.ac.uk> wrote:

> Thanks. Looks fine.
>
> What’s the situation with regard to regression testing? I know that there
> are scripts in developers/ for checking the entire system build.
>
> What I’d like a (relatively) quick way to check if basic encoder dependent
> stuff is working, i.e.
> • the low-level stages of compilation still evaluate (efficiently)
> • the translator still works (for the encoders)
>
> 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?
>
> Cheers,
> Anthony
>
> On 21 Dec 2016, at 22:37, Magnus Myreen <magnus.myreen at gmail.com> wrote:
>
> 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/20161223/cc05e401/attachment-0001.html>


More information about the Developers mailing list