disciple-cafe  

Messages by Thread

• patch ddc-head: SimpleRef: Shift extends into own module and fix admit in preservation Ben Lippmeier
• patch ddc-head: Proof: rename Nat module Ben Lippmeier
• patch ddc-head: SimpleRef: wibble Ben Lippmeier
• patch ddc-head: Proof: split list module into smaller parts Ben Lippmeier
• patch ddc-head: Add test/30-Runtime/DataR. Erik de Castro Lopo
• patch ddc-head: LLVM : Fix suspected heap corruption. Erik de Castro Lopo
• patch ddc-head: SimpleRef: finish eval minus list lemmas Ben Lippmeier
• patch ddc-head: SimpleRef: Add heap operations to big-step semantics Ben Lippmeier
• When is it safe to call _allocCollect? Erik de Castro Lopo
  • Re: When is it safe to call _allocCollect? Erik de Castro Lopo
  • Re: When is it safe to call _allocCollect? Ben Lippmeier
• patch ddc-head: SimpleRef: do big to small steps Ben Lippmeier
• patch ddc-head: SimpleRef: Fix admit in progress Ben Lippmeier
• patch ddc-head: SimpleRef: finish preservation bar list lemmas Ben Lippmeier
• patch ddc-head: SimpleRef: move forms of values into type module, and cleanup progress Ben Lippmeier
• patch ddc-head: SimpleRef: move dest and shift tactics into base library Ben Lippmeier
• patch ddc-head: SimpleRef: add main file Ben Lippmeier
• patch ddc-head: SimpleRef: fixing up automation Ben Lippmeier
• patch ddc-head: Simple: better automation Ben Lippmeier
• patch ddc-head: Simple: Extend burn tactic to be more useful Ben Lippmeier
• patch ddc-head: config-override.deps is now config-override.mk so we can clean *.deps and not lose it Ben Lippmeier
• patch ddc-head: war3: Remove unneeded canonicalizePaths Ben Lippmeier
• patch ddc-head: Move old war2 out of the way Ben Lippmeier
• patch ddc-head: Don't try to canonicalize paths to non-existant files Ben Lippmeier
• patch ddc-head: SimpleRef: Work on preservation Ben Lippmeier
• patch ddc-head: SimpleRef: exps, types and Progress Ben Lippmeier
• patch witness/witness-jfp: Edits benl
• patch witness/witness-jfp: Add JFP reviews benl
• Build broken on linux Ben Lippmeier
• patch ddc-head: Test needs to be updated for war3 Ben Lippmeier
• patch ddc-head: war3: allow failed tests to be dumped to file Ben Lippmeier
• patch ddc-head: These two tests don't work with the new driver Ben Lippmeier
• patch ddc-head: Rename normal -> std test way Ben Lippmeier
• patch ddc-head: Update other config files for new compilation setup Ben Lippmeier
• patch ddc-head: The old war is over Ben Lippmeier
• patch ddc-head: Remove debugging Ben Lippmeier
• patch ddc-head: war3: Don't show build dirs in test output paths Ben Lippmeier
• patch ddc-head: war3: also write output files into output dir for single compilation Ben Lippmeier
• patch ddc-head: Update test for new framework Ben Lippmeier
• patch ddc-head: Make LLVM produce the new compilation result structure Ben Lippmeier
• patch ddc-head: Move Result and Setup modules into DDC tree Ben Lippmeier
• patch ddc-head: Refactor management of files resulting from compilation Ben Lippmeier
• patch ddc-head: Make dump files go into the correct place Ben Lippmeier
• patch ddc-head: war3: whitespace Ben Lippmeier
• patch ddc-head: Better cleaning of test dir Ben Lippmeier
• patch ddc-head: Test wibble Ben Lippmeier
  • patch ddc-head: Test wibble Ben Lippmeier
• patch ddc-head: In progress adding outputdir flag Ben Lippmeier
• patch ddc-head: war3: put run.stderr.diff in build dir Ben Lippmeier
• patch ddc-head: Make proof build target work in parallel Ben Lippmeier
• patch ddc-head: Rename config-override.deps to config-override.mk Ben Lippmeier
• patch ddc-head: war3: Allow update of expected result for diff tests Ben Lippmeier
• patch ddc-head: war3: work on diff handling Ben Lippmeier
• patch ddc-head: war3: split gang controller into own module and start handling diffs Ben Lippmeier
• patch ddc-head: war3: handle run failure in pretty printer Ben Lippmeier
• patch ddc-head: war3: gang code is in buildbox now Ben Lippmeier
• patch ddc-head: war3: use /tmp dir for scratch space Ben Lippmeier
• patch ddc-head: war3: make ways work Ben Lippmeier
• patch ddc-head: Update testcase 10-Driver/EmptySourceFile to reflect the change to the error message. George Roldugin
• patch ddc-head: Follow-up for #219: Show filename of the bad source file. George Roldugin
• patch ddc-head: Fix #219: Fail source files containing no code or just comments (after lexing). George Roldugin
• patch ddc-head: #191: Update to work with war3 test driver Ben Lippmeier
• patch ddc-head: war3: wait for the controller to print all results before ending program Ben Lippmeier
• patch ddc-head: war3: don't build .ds files if there is a .sh script Ben Lippmeier
• patch ddc-head: runtime : Panic if the size of an object is zero. Erik de Castro Lopo
• patch ddc-head: runtime/Prim/Force.c : Include <assert.h> if _DDC_DEBUG is true. Erik de Castro Lopo
• patch ddc-head: war3: attach diff jobs to compile to ensure they're done in the correct order Ben Lippmeier
• patch ddc-head: war3: ease up on busy loop in gang controller Ben Lippmeier
• patch ddc-head: war3: handle shell tests that are expected to fail Ben Lippmeier
• patch ddc-head: war3: add shell tests Ben Lippmeier
• patch ddc-head: war3: add gang controller and flushing Ben Lippmeier
• patch ddc-head: war3: show compile time when compiling .hs files Ben Lippmeier
• patch ddc-head: war3: allow number of threads to be set on command line Ben Lippmeier
• patch ddc-head: In Core.ToSea, grab the Ctor parameter types from the Core data structures. Erik de Castro Lopo
• patch ddc-head: War3: Add thread gang to run tests in parallel Ben Lippmeier
• patch ddc-head: war3: update to use latest buildbox Ben Lippmeier
• patch ddc-head: library : Cast Float32# to Float64# before passing it to snprintf. Erik de Castro Lopo
• patch ddc-head: Add missing file. Erik de Castro Lopo
• patch ddc-head: library : Fix return types of foreign imported C functions. Erik de Castro Lopo
• patch ddc-head: LLVM : Special case runtime CAFs. Erik de Castro Lopo
• patch ddc-head: Make C SEEK_SET/CUR/END macros into CAFs in the runtime. Erik de Castro Lopo
• patch ddc-head: #155: update test file with more working example Ben Lippmeier
• patch ddc-head: SimpleData: add missing top-level file Ben Lippmeier
• patch ddc-head: Remove proof_old, all the proofs are in the main dir now Ben Lippmeier
• patch ddc-head: Fix #209: Simplify tagged closures including $Danger constructors Ben Lippmeier
• patch ddc-head: Handle zero-arity type constructors in new simplifier Ben Lippmeier
• patch ddc-head: Runtime : Fix compiler warning. Erik de Castro Lopo
• patch ddc-head: LLVM : Handle FFI C functons with void parameter list. Erik de Castro Lopo
• patch ddc-head: Add test/16-Core/T223-VoidParam. Erik de Castro Lopo
• patch ddc-head: Fix #223: Handle foriegn imported C functions that take zero parameters. Erik de Castro Lopo
• patch ddc-head: Add PAllocDataM primitive. Erik de Castro Lopo
• patch ddc-head: Main.Dump : Print name of file when dumping. Erik de Castro Lopo
• patch ddc-head: Fix #222: Disable tracing of unfinished constraint simplifier Ben Lippmeier
• patch ddc-head: SimpleData: shifting to use new framework Ben Lippmeier
• patch ddc-head: SimpleData: finish porting to new framework Ben Lippmeier
• patch ddc-head: SystemF2: port across to new framework Ben Lippmeier
• patch ddc-head: SimplePCF: port across to new framework Ben Lippmeier
• patch ddc-head: SystemF: Remove old makefile Ben Lippmeier
• patch ddc-head: SystemF: convert to new list library and cleanup Ben Lippmeier
• patch ddc-head: Wibble Ben Lippmeier
  • patch ddc-head: wibble Ben Lippmeier
  • patch ddc-head: wibble Ben Lippmeier
  • patch ddc-head: Wibble Ben Lippmeier
  • patch ddc-head: Wibble Ben Lippmeier
  • patch ddc-head: wibble Tran Ma
  • patch ddc-head: wibble Ben Lippmeier
• patch ddc-head: Remove old simple proof dir Ben Lippmeier
• patch ddc-head: Simple: docs and cleanups Ben Lippmeier
• patch ddc-head: Simple: Rename modules Ben Lippmeier
• patch ddc-head: Add missing proof.mk file Ben Lippmeier
• patch ddc-head: Proof: Stifle warnings about notations as keywords Ben Lippmeier
• patch ddc-head: Simple: follow changes in base library Ben Lippmeier
• patch ddc-head: Add proofs to makefile. Use "make proof" Ben Lippmeier
• patch ddc-head: Shift proof dir Ben Lippmeier
• patch ddc-head: Simple: Redo environment library to be based on Coq lists Ben Lippmeier
• patch ddc-head: Simple Data: finish XCon context stuff, ffs. Ben Lippmeier
• patch ddc-head: Simple Data: delete old broken context lemmas Ben Lippmeier
• patch ddc-head: Simple Data: Redoing big-step eval for XCon to use EVALS judgement Ben Lippmeier
• #223 Unboxed constructors Erik de Castro Lopo
  • Re: #223 Unboxed constructors Ben Lippmeier
• patch ddc-head: Source.Lint : Remove check for boxed and unboxed fields in a constructor. Erik de Castro Lopo
• patch ddc-head: Set default number of threads to 1, to avoid build races in buildbots Ben Lippmeier
• patch ddc-head: Simple Data: add cuts file of leftover stuff Ben Lippmeier
• patch ddc-head: Simple Data: fix admit in EvJudge Ben Lippmeier
• patch ddc-head: Simple Data: result type of a data constructor is a data type constructor Ben Lippmeier
• patch ddc-head: Simple Data: fix progress for case exps Ben Lippmeier
• patch ddc-head: Simple Data: fix progress, but breaks expansion Ben Lippmeier
• patch ddc-head: Simple Data: fix admit in Progress Ben Lippmeier
• patch ddc-head: Simple Data: fix progress in case context Ben Lippmeier
• patch ddc-head: Simple Data: tag of data con must belong to the corresponding type con Ben Lippmeier
• patch ddc-head: Simple Data: Fix preservation for XCon Ben Lippmeier
• patch ddc-head: Whitespace cleanup. Erik de Castro Lopo
  • patch ddc-head: Whitespace cleanup. Erik de Castro Lopo
• patch ddc-head: Plumbing for constructors with unboxed fields. Erik de Castro Lopo
• patch ddc-head: Simple Data: go back to exps contexts as a list Ben Lippmeier
• patch ddc-head: Simple Data: fix EvJudge lemmas for XCon with list contexts Ben Lippmeier
• patch ddc-head: Simple Data: don't require a value when nf will do Ben Lippmeier
• patch ddc-head: library/Base.ds : Add a Void constructor to the Void# type. Erik de Castro Lopo
• patch ddc-head: Simple Data: fix context lemma Ben Lippmeier
• patch ddc-head: Simple Data: fix context swap lemma Ben Lippmeier
• patch ddc-head: Simple Data: move lemma Ben Lippmeier
• patch ddc-head: Simple Data: Split out alternative utils into their own module Ben Lippmeier
• patch ddc-head: Simple Data: split out context defs into their own module Ben Lippmeier
• patch ddc-head: Simple Data: move lemmas around Ben Lippmeier
• patch ddc-head: Simple Data: more work on contexts for XCon Ben Lippmeier
• patch ddc-head: Simple Data: add cuts for leftover stuff Ben Lippmeier
• patch ddc-head: Simple Data: rename module Ben Lippmeier
• patch ddc-head: Simple Data: finish splitAt shift lemma Ben Lippmeier
• patch ddc-head: Simple Data: finish take_step lemma Ben Lippmeier
• patch ddc-head: Simple Data: add more lemmas about take Ben Lippmeier
• patch ddc-head: Simple Data: redo def of splitAt to use take, drop Ben Lippmeier
• patch ddc-head: Simple Data: in progress Ben Lippmeier
  • patch ddc-head: Simple Data: in progress Ben Lippmeier
• patch ddc-head: T163 Elaboration of classes with specified regions - incomplete pattern match Amos Robinson
• patch ddc-head: Simple Data: do eval_expansion for case Ben Lippmeier
• patch ddc-head: Simple Data: add eval in case discrim and steps_of_eval for case Ben Lippmeier
• T163 Elaboration of classes with specified regions Amos Robinson
  • Re: T163 Elaboration of classes with specified regions Erik de Castro Lopo
  • Re: T163 Elaboration of classes with specified regions Amos Robinson
  • Re: T163 Elaboration of classes with specified regions Erik de Castro Lopo
  • Re: T163 Elaboration of classes with specified regions Ben Lippmeier
  • Re: T163 Elaboration of classes with specified regions Amos Robinson
  • Re: T163 Elaboration of classes with specified regions Erik de Castro Lopo
  • Re: T163 Elaboration of classes with specified regions Amos Robinson
  • Re: T163 Elaboration of classes with specified regions Ben Lippmeier
  • Re: T163 Elaboration of classes with specified regions Ben Lippmeier
  • Re: T163 Elaboration of classes with specified regions Ben Lippmeier
• patch ddc-head: T163 Elaboration of classes with specified regions Amos Robinson
  • patch ddc-head: T163 Elaboration of classes with specified regions Amos Robinson
• patch ddc-head: Simple Data: cleanup big step evaluation. It's not finished yet though. Ben Lippmeier
• patch ddc-head: Simple Data: remove old, unused test module Ben Lippmeier
• patch ddc-head: Simple Data: flesh out progress theorem Ben Lippmeier
• patch ddc-head: Simple Data: finish simultaneous substitution lemma for case alternatives Ben Lippmeier
• patch ddc-head: Simple Data: dump unused lemmas Ben Lippmeier
• patch ddc-head: Simple Data: Preservation bits Ben Lippmeier
• patch ddc-head: Simple Data: map_length is in the standard library Ben Lippmeier
• patch ddc-head: Simple Data: add datacon_beq and fix admit Ben Lippmeier
• patch ddc-head: Simple Data: finish most of Preservation Ben Lippmeier
• patch ddc-head: Update .authorspellings. Erik de Castro Lopo
• patch ddc-head: Fix #224: Accept both '42i64#' and '42#i64' as unboxed hex literals. Erik de Castro Lopo
• patch ddc-head: Whitespace only. Erik de Castro Lopo
  • patch ddc-head: Whitespace only. Erik de Castro Lopo
• patch ddc-head: Simple Data: preservation case for constructor evaluation Ben Lippmeier
• patch ddc-head: Simple Data: add evaluation contexts Ben Lippmeier
• patch ddc-head: Simple Data: Add eval rules for case expressions Ben Lippmeier
• Can't figure how to fix Docable Erik de Castro Lopo
  • Re: Can't figure how to fix Docable Erik de Castro Lopo
  • Re: Can't figure how to fix Docable Ben Lippmeier
  • Re: Can't figure how to fix Docable Erik de Castro Lopo
• patch ddc-head: Simple PCF: Finish conversion to use evaluation contexts Ben Lippmeier
• patch ddc-head: Simple PCF: Start converting evaluation to use contexts Ben Lippmeier
• patch ddc-head: Add runtime debug functions ddcObjAddress, ddcPointerDiff. Erik de Castro Lopo
• patch ddc-head: Sea.Pretty : Use 'void' for functions with empty parameter lists. Erik de Castro Lopo
• patch ddc-head: Simple: Rename Env -> BaseEnv Ben Lippmeier
• patch ddc-head: Simple: Rename modules using contexts to be the real versions Ben Lippmeier
• patch ddc-head: Simple: Ditch non-context versions Ben Lippmeier
• patch ddc-head: Simple: Add big-step eval using contexts Ben Lippmeier
• patch ddc-head: Simple: Add progress and preservation using evaluation contexts Ben Lippmeier
• patch ddc-head: Simple Data: use induction using syntax instead of explicitly applying induction scheme Ben Lippmeier
• patch ddc-head: Simple Data: finish liftX_succ Ben Lippmeier

• Earlier messages
• Later messages