disciple-cafe  

Messages by Thread

• patch ddc-head: Simple Data: finish apppend env lemmas for subst exp/exp Ben Lippmeier
• patch ddc-head: Simple Data: Add more liftX lemmas and fix type_tyenv_weaken_append Ben Lippmeier
• patch ddc-head: Simple Data: Split Exp into more modules Ben Lippmeier
• patch ddc-head: Simple Data: Prove liftX_zero Ben Lippmeier
• patch ddc-head: Simple Data: Do most of subst exp/exp minus lemmas Ben Lippmeier
• patch ddc-head: Simple Data: Add missing Makefile Ben Lippmeier
• patch ddc-head: Simple Data: Do most of Subst Exp/Exp need to generalise liftX to push all ctor args on env at once Ben Lippmeier
• patch ddc-head: Simple Data: Use Forall instead of In in TyJudge Ben Lippmeier
• patch ddc-head: Simple Data: finish Forall / Forall2 lemmas Ben Lippmeier
• patch ddc-head: Simple Data: Finish type_tyenv_weaken minus Forall lemmas Ben Lippmeier
• patch ddc-head: Simple Data: working on relational stuff in type_tyenv_insert Ben Lippmeier
• patch ddc-head: Finish Forall2 lemma for wfX Ben Lippmeier
• patch ddc-head: Add comment about induction principle Ben Lippmeier
• patch ddc-head: Simple Data: Add data constructor args to env during case match Ben Lippmeier
• patch ddc-head: Add induction principle for expressions Ben Lippmeier
• patch ddc-head: Use In predicate to manage lists in Simple_Data Ben Lippmeier
• patch ddc-head: Fix #213 Name Clash: Make sure CAFs are not multiply defined Amos Robinson
• patch ddc-head: Fix #213 Name Clash: Add source position to foreign import bindings Amos Robinson
• DDC Build (deluge.linux-x86.head) failure DDC BuildBot
  • DDC Build (deluge.linux-x86.head) failure DDC BuildBot
• patch ddc-head: Formatting only Ben Lippmeier
• Trac user registration Amos Robinson
  • Re: Trac user registration Erik de Castro Lopo
• patch ddc-head: Fix #213: Raise error in Renamer on function name clashes. Amos Robinson
• patch ddc-head: Add new exp cases for Simple Data Ben Lippmeier
• patch ddc-head: Only OSX needs the as -arch flag Ben Lippmeier
• patch ddc-head: Enable llvm in during testing Ben Lippmeier
• patch ddc-head: Dup Simple proof as Simple_Data Ben Lippmeier
• patch ddc-head: Follow changes in other config files Ben Lippmeier
• patch ddc-head: library/ : Add pointerSize to System.Environment. Erik de Castro Lopo
• Bug #213 Name clashes on foreign imports Amos Robinson
  • Re: Bug #213 Name clashes on foreign imports Erik de Castro Lopo
  • Re: Bug #213 Name clashes on foreign imports Amos Robinson
  • Re: Bug #213 Name clashes on foreign imports Erik de Castro Lopo
  • Re: Bug #213 Name clashes on foreign imports Erik de Castro Lopo
  • Re: Bug #213 Name clashes on foreign imports Amos Robinson
  • Re: Bug #213 Name clashes on foreign imports Ben Lippmeier
  • Re: Bug #213 Name clashes on foreign imports Ben Lippmeier
  • Re: Bug #213 Name clashes on foreign imports Ben Lippmeier
  • Re: Bug #213 Name clashes on foreign imports Ben Lippmeier
• patch ddc-head: Rename XArgData constructor to XArgBoxedData. Erik de Castro Lopo
• patch ddc-head: Add unboxed version of XArgBoxedData constructor, XArgUnboxedData. Erik de Castro Lopo
• patch ddc-head: Finish PCF Progress Ben Lippmeier
• patch ddc-head: Use Coq Nat instead of Succ to represent naturals in Simple_PCF Ben Lippmeier
• patch ddc-head: Do most of PCF expansion lemma Ben Lippmeier
• patch ddc-head: Fix PCF preservation Ben Lippmeier
• patch ddc-head: Add extra type and evaluation rules for PCF Ben Lippmeier
• patch ddc-head: LLVM : Remove unused isUnboxed predicate. Erik de Castro Lopo
• patch ddc-head: Use library comparison instead of BaseCompare Ben Lippmeier
• patch ddc-head: Dup Simple proof as Simple_PCF Ben Lippmeier
• patch ddc-head: make/targets/libs.mk : Add $(config_ddc_flags) to bin/ddc command lines. Erik de Castro Lopo
• Bug #223 : Type mismatch with foriegn import of C functions that take zero parameters Erik de Castro Lopo
  • Re: Bug #223 : Type mismatch with foriegn import of C functions that take zero parameters Ben Lippmeier
• patch ddc-head: Dup SystemF proof as SystemF2 Ben Lippmeier
• patch ddc-head: Update kind and type structure for SystemF2 Ben Lippmeier
• patch ddc-head: Finish changes for SystemF2 Ben Lippmeier
• patch ddc-head: Fix type_kind for SystemF2 Ben Lippmeier
• patch ddc-head: Fix SystemF2 subst type/type Ben Lippmeier
• patch ddc-head: update makefile Ben Lippmeier
• patch ddc-head: Do big to small step evaluation for SystemF Ben Lippmeier
• patch ddc-head: Do big step eval for SystemF and big to small steps lemma Ben Lippmeier
• patch ddc-head: Use whnf to define value in SystemF Ben Lippmeier
• patch ddc-head: Port multistep stuff from Simple into SystemF Ben Lippmeier
• patch ddc-head: Comments and cleanup Ben Lippmeier
• patch ddc-head: Docs and cleanups to Simple proof Ben Lippmeier
• patch ddc-head: Add Simple stepsl_to_eval Ben Lippmeier
• patch ddc-head: Fix Simple expansion lemma Ben Lippmeier
• patch ddc-head: Do most of expansion lemma for Simple Ben Lippmeier
• patch ddc-head: Working on small to big step evaluation Ben Lippmeier
• patch ddc-head: Lint : Raise error if Ctors contain a mixture of boxed and unboxed fields. Erik de Castro Lopo
• patch ddc-head: Whitespace. Erik de Castro Lopo
  • patch ddc-head: Whitespace. Erik de Castro Lopo
  • patch ddc-head: Whitespace. Erik de Castro Lopo
  • patch ddc-head: Whitespace. Erik de Castro Lopo
  • patch ddc-head: Whitespace. Erik de Castro Lopo
• patch ddc-head: Add Simple makefile, and cleanups Ben Lippmeier
• Can now build the library using -fvia-llvm Erik de Castro Lopo
• patch ddc-head: LLVM : Handle Int8#, Int16# and Word16#. Erik de Castro Lopo
• patch ddc-head: LLVM : Finish handling of PExterns. Erik de Castro Lopo
• patch ddc-head: LLVM : In addGlobalVar compare LlvmType instead of whole LlvmVar. Erik de Castro Lopo
• patch ddc-head: DDC.Core.ToSea : Special case toSeaT for PExterns as toSeaExternT. Erik de Castro Lopo
• patch ddc-head: LLVM : Generate global LlvmVar for each PExtern decl. Erik de Castro Lopo
• patch ddc-head: LLVM : Fix isGlobalVar so it checks the bound variable as well. Erik de Castro Lopo
• patch ddc-head: Parser : Tag foreign imported data with 'ISeaGlobal True'. Erik de Castro Lopo
• patch ddc-head: Do big to small step evaluation for Simple Ben Lippmeier
• patch ddc-head: Rename Simple EvJudge to EsJudge. We'll use the former for big-step reduction. Ben Lippmeier
• patch ddc-head: Add PExtern constructor to Sea's Top data structure. Erik de Castro Lopo
• patch ddc-head: Fix T191-LocalMake on OSX. Erik de Castro Lopo
• patch ddc-head: test/15-Typing/01-StandAlone/Eq/Test.ds : Remove redundant CoercePtr. Erik de Castro Lopo
• patch ddc-head: Reorganise SystemF proof Ben Lippmeier
• patch ddc-head: Remove unused proof bits Ben Lippmeier
• patch ddc-head: Ditch Simple proof using explicit names Ben Lippmeier
• patch ddc-head: Rename Poly back to SystemF Ben Lippmeier
• patch ddc-head: Ditch broken poly proof using explicit names Ben Lippmeier
• patch ddc-head: Prove poly preservation Ben Lippmeier
• Running war driver with the llvm backend Erik de Castro Lopo
  • Re: Running war driver with the llvm backend Ben Lippmeier
  • Re: Running war driver with the llvm backend Ben Lippmeier
• patch ddc-head: make/ : Add $(compway_llvm) variable to 'totallogwar' target. Erik de Castro Lopo
• DDC Build (corea.linux-ppc.head) failure Erik's DDC BuildBot
  • DDC Build (corea.linux-ppc.head) failure Erik's DDC BuildBot
  • DDC Build (corea.linux-ppc.head) failure Erik's DDC BuildBot
• patch ddc-head: LLVM : Fix codegen for 64 bit literals on 32 bit systems. Erik de Castro Lopo
• patch ddc-head: DDC.Type.Simplify : Improve panic message. Erik de Castro Lopo
• patch ddc-head: Change -via-llvm command line options to -fvia-llvm. Erik de Castro Lopo
• patch ddc-head: LLVM : Add float cast operations. Erik de Castro Lopo
• patch ddc-head: LLVM : More stdin/stdout/stderr FILE handling. Erik de Castro Lopo
• Foreign imports and the LLVM backend Erik de Castro Lopo
  • Re: Foreign imports and the LLVM backend Erik de Castro Lopo
• patch ddc-head: LLVM : Special case stdin, stdout and stderr FILE handles. Erik de Castro Lopo
• patch ddc-head: Start on poly progress, fix WellFormed Ben Lippmeier
• patch ddc-head: Finish poly progress Ben Lippmeier
• patch ddc-head: System.Console.fputsU_console returns Int32#, not Int. Erik de Castro Lopo
• patch ddc-head: LLVM : Hmm, handle Addr#, but add comments about better future solution. Erik de Castro Lopo
• patch ddc-head: LLVM : Implement OpIsZero. Erik de Castro Lopo
• patch ddc-head: LLVM : Make type of size parameter to snprintf() i32. Erik de Castro Lopo
• patch ddc-head: LLVM : Add primAllocDataR. Erik de Castro Lopo
• patch ddc-head: Do most of poly subst value/value Ben Lippmeier
• patch ddc-head: Finish poly subst value/value Ben Lippmeier
• patch ddc-head: Drop separate liftTT' and substTT' functions Ben Lippmeier
• patch ddc-head: LLVM : For special case varags functions look up the Sea name. Erik de Castro Lopo
• patch ddc-head: LLVM : Add support for peeking an poking on Float data. Erik de Castro Lopo
• patch ddc-head: LLVM : Handle calling of functions returning Void#. Erik de Castro Lopo
• patch ddc-head: LLVM : Clean up primitive Ptr operations. Erik de Castro Lopo
• patch ddc-head: Add support for PrimPtrPeek. Erik de Castro Lopo
• patch ddc-head: LLVM : Handle peekDataR_payload. Erik de Castro Lopo
• patch ddc-head: LLVM : Extend PrimPtrPoke and PrimPtrPokeOn support. Erik de Castro Lopo
• patch ddc-head: LLVM : Add primitives arrayUI_peek and arrayUI_poke. Erik de Castro Lopo
• patch ddc-head: LLVM : Implement llvmOfSStmt in terms of llvmOfExp to reduce code duplication. Erik de Castro Lopo
• patch ddc-head: Finish lemmas Poly subst type/value Ben Lippmeier
• patch ddc-head: LLVM : Add definition of ddcDataR. Erik de Castro Lopo
• Re: Honours at UNSW Erik de Castro Lopo
  • Re: Honours at UNSW Amos Robinson
  • Re: Honours at UNSW Erik de Castro Lopo
• DDC Build (corea.linux-ppc.head) success Erik's DDC BuildBot
  • DDC Build (corea.linux-ppc.head) success Erik's DDC BuildBot
  • DDC Build (corea.linux-ppc.head) success Erik's DDC BuildBot
  • DDC Build (corea.linux-ppc.head) success Erik's DDC BuildBot
  • DDC Build (corea.linux-ppc.head) success Erik's DDC BuildBot
  • DDC Build (corea.linux-ppc.head) success Erik's DDC BuildBot
  • DDC Build (corea.linux-ppc.head) success Erik's DDC BuildBot
  • DDC Build (corea.linux-ppc.head) success Erik's DDC BuildBot
  • DDC Build (corea.linux-ppc.head) success Erik's DDC BuildBot
  • DDC Build (corea.linux-ppc.head) success Erik's DDC BuildBot
  • DDC Build (corea.linux-ppc.head) success Erik's DDC BuildBot
  • DDC Build (corea.linux-ppc.head) success Erik's DDC BuildBot
  • Re: DDC Build (corea.linux-ppc.head) success Erik de Castro Lopo
  • Re: DDC Build (corea.linux-ppc.head) success Ben Lippmeier
  • DDC Build (corea.linux-ppc.head) success Erik's DDC BuildBot
  • DDC Build (corea.linux-ppc.head) success Erik's DDC BuildBot
  • DDC Build (corea.linux-ppc.head) success Erik's DDC BuildBot
  • DDC Build (corea.linux-ppc.head) success Erik's DDC BuildBot
  • DDC Build (corea.linux-ppc.head) success Erik's DDC BuildBot
  • DDC Build (corea.linux-ppc.head) success Erik's DDC BuildBot
  • DDC Build (corea.linux-ppc.head) success Erik's DDC BuildBot
  • DDC Build (corea.linux-ppc.head) success Erik's DDC BuildBot
  • DDC Build (corea.linux-ppc.head) success Erik's DDC BuildBot
  • DDC Build (corea.linux-ppc.head) success Erik's DDC BuildBot
  • DDC Build (corea.linux-ppc.head) success Erik's DDC BuildBot
  • DDC Build (corea.linux-ppc.head) success Erik's DDC BuildBot
  • DDC Build (corea.linux-ppc.head) success Erik's DDC BuildBot
  • DDC Build (corea.linux-ppc.head) success Erik's DDC BuildBot
  • DDC Build (corea.linux-ppc.head) success Erik's DDC BuildBot
  • DDC Build (corea.linux-ppc.head) success Erik's DDC BuildBot
  • DDC Build (corea.linux-ppc.head) success Erik's DDC BuildBot
  • DDC Build (corea.linux-ppc.head) success Erik's DDC BuildBot
  • DDC Build (corea.linux-ppc.head) success Erik's DDC BuildBot
• DDC Build (freebsd8-32.freebsd8-x86.head) success Erik's DDC BuildBot
  • DDC Build (freebsd8-32.freebsd8-x86.head) success Erik's DDC BuildBot
  • DDC Build (freebsd8-32.freebsd8-x86.head) success Erik's DDC BuildBot
  • DDC Build (freebsd8-32.freebsd8-x86.head) success Erik's DDC BuildBot
  • DDC Build (freebsd8-32.freebsd8-x86.head) success Erik's DDC BuildBot
  • DDC Build (freebsd8-32.freebsd8-x86.head) success Erik's DDC BuildBot
  • DDC Build (freebsd8-32.freebsd8-x86.head) success Erik's DDC BuildBot
  • DDC Build (freebsd8-32.freebsd8-x86.head) success Erik's DDC BuildBot
  • DDC Build (freebsd8-32.freebsd8-x86.head) success Erik's DDC BuildBot
  • DDC Build (freebsd8-32.freebsd8-x86.head) success Erik's DDC BuildBot
  • DDC Build (freebsd8-32.freebsd8-x86.head) success Erik's DDC BuildBot
  • DDC Build (freebsd8-32.freebsd8-x86.head) success Erik's DDC BuildBot
  • DDC Build (freebsd8-32.freebsd8-x86.head) success Erik's DDC BuildBot
  • DDC Build (freebsd8-32.freebsd8-x86.head) success Erik's DDC BuildBot
  • DDC Build (freebsd8-32.freebsd8-x86.head) success Erik's DDC BuildBot
  • Re: DDC Build (freebsd8-32.freebsd8-x86.head) success Erik de Castro Lopo
  • Re: DDC Build (freebsd8-32.freebsd8-x86.head) success Ben Lippmeier
  • DDC Build (freebsd8-32.freebsd8-x86.head) success Erik's DDC BuildBot
  • DDC Build (freebsd8-32.freebsd8-x86.head) success Erik's DDC BuildBot
  • DDC Build (freebsd8-32.freebsd8-x86.head) success Erik's DDC BuildBot
  • Re: DDC Build (freebsd8-32.freebsd8-x86.head) success Erik de Castro Lopo
  • DDC Build (freebsd8-32.freebsd8-x86.head) success Erik's DDC BuildBot
  • DDC Build (freebsd8-32.freebsd8-x86.head) success Erik's DDC BuildBot
  • DDC Build (freebsd8-32.freebsd8-x86.head) success Erik's DDC BuildBot
  • DDC Build (freebsd8-32.freebsd8-x86.head) success Erik's DDC BuildBot
  • DDC Build (freebsd8-32.freebsd8-x86.head) success Erik's DDC BuildBot
  • Re: DDC Build (freebsd8-32.freebsd8-x86.head) success Erik de Castro Lopo
  • DDC Build (freebsd8-32.freebsd8-x86.head) success Erik's DDC BuildBot
  • Re: DDC Build (freebsd8-32.freebsd8-x86.head) success Ben Lippmeier
  • Re: DDC Build (freebsd8-32.freebsd8-x86.head) success Erik de Castro Lopo
  • Re: DDC Build (freebsd8-32.freebsd8-x86.head) success Ben Lippmeier
  • DDC Build (freebsd8-32.freebsd8-x86.head) success Erik's DDC BuildBot
  • DDC Build (freebsd8-32.freebsd8-x86.head) success Erik's DDC BuildBot

• Earlier messages
• Later messages