Skip to content

Meeting Notes

Jump to bottom
Shon Feder edited this page May 10, 2021 · 30 revisions

Apalache Meeting Log

Sticky note (do not move): Let's keep it simple. The meeting agenda and notes go in this file. The updates to this file are made via GitHub pull requests. By doing so, we make sure that:

  • All team members have a chance to see the updates, via the GitHub interface,
  • All team members may add their points to the agenda and meeting notes,
  • We use the tools that we master (our text editors and GitHub),
  • We do not have to transfer the common knowledge between email, notion, roam, google docs, or whatever comes next.

Apalache Meeting Notes

Strategy - 2021.05.03

Customer updates

  • Andrey: What is status with respect to MBT support?
    • Unit testing
    • Concerned about deprioritizing of 542 (--continue)
      • Igor: We aim to support that as a special use-case of the server mode.
      • Andrey: Concerned that it would be easier and faster to implement #542 rather than wait for the server mode to be implemented.
    • What is MBT timeline and need for the feature in #542
      • By end of Q2
      • Shon: Are you currently blocked on this?
    • Can use randomization and guided search for short term:
    • Needs transitions &
    • If MBT has support for this, we can start uncovering subtle bugs
      • Igor: Can't you start uncovering subtle bugs already?
    • MBT wants to be able to programmatically call transition executor API
      • Igor: JSON server seams like the right way to provide this.
      • How long will it take us to implement?
        • Igor:
          • ~1 week For very simple prototype
          • Much longer for robust implementation
        • Shon: Could we do a spike on this for 2 weeks?
        • We all have audits pending
    • Alternative: just provide number of transitions, would have MBT OK for now.
      • How difficult?
        • Add one operator to record NTransitions == n
    • Jure:
      • Availability: may suspend contract work in May.
    • Conclusion:
      • MBT will try using random mode, if this is good enough, that will be the short-term solution.
        • Also, in the mean time, MBT has bug fixes and hardening of architecture to work on.
      • If MBT is stuck, we'll implement a special feature, which is just a workaround, with the understanding that it will be going away in Q3
        • TODO: Check in next week
      • In the meantime, we'll continue prioritizing the "correct" implementation
      • Meta:
        • In coordinating work, MBT side shouldn't have to be concerned with our implementation strategies (tho of course substantive input on architectural decisions is welcome)
        • Rather, they can/should let us know their time lines and what they need, and we can estimate and commit to delivering certain features to meet the needs.
    • What's the current bottleneck for finding bugs?
      • We're not providing the coverage we could be with MBT, because only checking one possible point in the search space.
      • Developers are using MBT, an surprised there is no automated searching of space of behaviors.

Plans

  • Jure will be out this month to focus on thesis
    • Will finish the JSON reader in the meantime.
      • TODO Shon: Tell Andrey that we are deleting the old JSON serialization format.
    • Will open issue on ADR for package/module restructuring
  • Igor: working on prototype for unit testing
    • Will spend 1-2 days, and postpone if it doesn't converge.
    • Start writing a proposal on the server architecture
  • Shon:
    • ADR for server/daemon mode
      • Take current checker module, but instead of running it, start a server, a process queries to the transition executor (specified in ADR3)
      • Let's also bake in support for LSP protocol support.
      • Should also feed into online use
      • Should feed into REPL usage?
      • RPC into the transition executor ADR
        • Gives us more incrementality
        • Will let us roll back and take different steps
        • Let's us expose the "symbolic execution" functionality
          • We're actually doing symbolic execution, but even more powerfully than many applications (because we explore branches)
      • Aim is to avoid adding too m
      • Let's aim for a deep API
      • Symbolic model checking is very easy, in a sense.
        • Not so much to it.
        • Once we have the translation into SMT, the model checking is simple.
      • Recalling the DFS mode we had before
    • Tutorial on transition from basic TLA+ knowledge to basic use of Apalache.

re: Strategy

  • We'll have prototyping features of both high priority strategies
  • Most stretch goals will not be met

Other topics

  • How can we reduce the size of the IR?
    • Open issue to say "Remove toString" from the IR

Standup - 2021.04.26

Last week

  • Igor:
    • User Stories
      • First draft
      • Needs review and more input?
      • Not clear on all goals
    • How are the personae supposed to guide us?
      • We identify which ones we want to support and which ones we don't really want to support.
      • When people ask us to support someone in the future, we can use it to identify people we don't want to support.
      • Meant to help us stay in focus.
        • When anyone wants to add a new feature, we can determine which persona we want to add.
  • Shon:
    • Some CI cludge.
      • Time for some touch up work here?
      • Might we postpone until Q3?
  • The need for incremental changes
    • We should clarify exactly what we need here, who it supports, and how.
    • Maybe we need to rethink the way we are doing transformation passes?
      • The more optimizations we add the more problems we add.
    • Jure:
      • We should be able to do transformations locally, if we just change our current approach.
    • Igor: Let's look at static analysis techniques
    • Jure:
      • Our current unit of compilation is a module.
      • But if we narrow our unit of compilation, we should get this locality.
    • Jure:
      • Let's not implement this until we have a proper discussion of architecture.
      • All agreed.
    • Let's keep this in mind, and gather ideas/approaches
      • Let's make an issue, and let ideas percolate
      • This is related to the server but as an eventual enhancement, not as a blocking requirement
  • PIWEEK
    • Igor
  • Jure
    • Working on the self-typing builder
      • Trouble using Etc
        • Some unimplemented operators.
        • Indicates a need for a different approach to the Etc API.
  • re: refactoring
    • we have significant pressure to implement new features
    • Jure:
      • should budget time to fix existing issues
    • Igor:
      • we need to sell our refactoring
    • Shon:
      • But there should be room for working driven by passion/interest/felt need.

This week

Standup - 2021.04.19

Last week

  • JSON Adr merged in
  • Release process is still brittle :(

This week

  • Jure:
    • Self-typing builder? How to move forward?
      • Add the Etc expression into the same PR
      • Does this fit with our current priorities?
        • Will spike on that this week.
        • If not done by next week, we'll consider postponing.
    • Look into ser/de libraries for Scala, can we use this for the JSON ADR
      • Pick a maintained library
      • Let's do some exploratory work on this
  • Igor:
    • Continuing work on testing RFC
      • Testing looks like its becoming a way to help guide us towards compositional specs?
  • Shon:
    • Should find a feature or issue to guide deeper engagement
    • Otherwise, won't do much due to piweek focus.

Standup - 2021.04.12

  • Prioritizing support for MBT and TLA+ Unit testing (using generators)

Last week

  • Igor:
    • Testing generators
      • Needs feedback/insight from user support
    • Refactoring IR, renaming operators
    • Refactoring formal params
  • Jure: Json ADR refinement
    • Under view and editing
  • Shon: Releasing artifacts with no version suffix

This week

Strategy - 2021.04.06

This milestone: https://github.com/informalsystems/apalache/milestone/32

Aim this month

  • Get the Alpha out

Usability issues for release?

  • We need to improve our UI concern
    • TODO(Shon) See "The Inmates are Running the Asylum"
      • Engineers tend to build things around what are easy to implement rather than what is best for users etc.
      • Don't design your tools for experts or beginners, but for avg users.
  • TODO(All) We need to figure out who are our users:
    • Who do we believe our users will be?
    • What do I want to do as a user?
      • Assume you know how to write TLA.
      • Assume you have Apalache.
      • What do you expect from this tool?
    • Our default mode has been:
      • Assumption has been: People want to write a spec to do a complete (or partial) verification.
      • But, many people just want to
        • Document
        • Explore
        • Think through things
    • Need to write down different user profiles
      • Let's find out the user profiles
      • Let's then make decisions about the ones we want to support
      • What about a user survey?
        • "Survivors" vs "apologists"
          • Apologists are louder
          • Survivors tend to be quiter, and sometimes ashamed of the places they have difficulty
        • come up with questionaire
          • What do you do with it?
          • What do you want to do with it?
          • How long have you been using it?
          • What do you use it for?
          • Industry?
          • Esp. target non-users, people who are interested but have been blocked or not quite enough to do.
            • We want to find out what they are using it for.
        • Share draft with TLC folks to see if they have any input.
      • Shon: The primary interface to the language is the language itself.
        • let's keep in mind improvements/revisions to the language, that compile into our IR or the SMT arenas.
        • We all agree this is on the roadmap, but it's some way down the line
    • Invariants all users want to do:
      • Jure: Execute the spec
        • But because operators are not compositional in terms of the property we're trying to check, users can't develop in the way they usually do, which is write composable bits, try them, and then iterate and incrementally proceed.
        • Igor: Something like unit or PBT tests etc.
        • Debugging in isolation would help understand what's going
      • Improved support for compositionality
        • If users can check operators in isolation and they gradually refine the inputs, they'll likely end up converging upon inductive invariants.
        • Currently trying to find inductive invariants is not very interactive.
          • Something like REPL feedback?
        • Easier for Apalache to check things locally than globally
      • What is like Hoare calculus in TLA
      • What is it that makes compositionality hard in TLA
        • Actions? (Global state and its transitions)
      • Any value to focusing on "instantaneous" and/or "pure" formulas?
        • Formulas:
          • Constant
          • State level
          • Action level
  • Shon: "Cloud Model Checking"
    • Hash specs, then see if we have already existing traces.
    • Igor: CF Unison
      • Knowledge keeps accumulating
      • Caching results (accumulating)

Action items

Standup - 2021.03.29

Last week

  • Igor - Still integrating snowcat
  • Jure - Typed builder
  • Shon - Tracer (and some code review)

This week

  • Igor
    • Adding tutorial on types to documentation.
      • Geared towards people who don't know how to write types.
      • Some issues cleanup.
    • Issues with recursive operators.
      • Our elements are not ordered.
        • If our elements were ordered, we could improve, but how do we order things like functions or records?
      • We'll not deal with this until after the release.
  • Jure
    • Wrap up JSON ADR (+ new feature implementation)
      • Deserialization
        • Will need validation for reading in?
        • We'll need to report decent error messages for nonsense ASTs
        • Can implement this stuff incrementally
      • Do we need to preserve the source info that may be present in the JSON in the Scala AST?
        • Possible uses: E.g., someone is generating JSON representation of TLA with a python function, wants to record the "source location" as the part of the python code that produces the expression.
          • Shon: But then we're overloading the meaning of this field in the Scala data structures: sometimes it would mean source file location sometimes it would mean generating function location?
        • Let's just make an issue, and we can discuss if needed and if so, how to implement.
        • Let's ignore this for first implementation.
    • SFP / OFP unification
    • JSON Reader
  • Shon
    • Hoping to spend some time at end of week on packaging.
    • Needs to cut release.
    • Address some brittleness in release pipeline.
      • Not sure how off the top of my head...

Additional items

  • Pandemic is still bad :(
    • But less sticks in nose on TV please
  • Strategy meeting?
    • next one is on a Holiday.
    • Let's move it to Tuesday
      • Plan what to propose for our Q2 work
      • Also discuss what is blocking Alpha release
  • "Super suboptimal"
    • Joseph: is this "optimal" or sub-suboptimal.

Retro - 2021.03.25

Went well

  • Integration of snowcat
    • Making TLA+ feel like a programming language :)
  • Igor: we get more user feedback
  • refactoring and bugfixes

Didn't go well

  • "Heroic feats"
  • Didn't open space for retro ideation in advance
  • Old decisions are catching up to us? (maybe neutral)
    • From learning more about language.
    • Natural improvements

To improve

  • Avoiding heroic feats/burnout
    • Don't commit to present on things not finished
    • We should have our own timelines
    • We shouldn't be afraid of pushing back deadlines when necessary
    • Make sure to talk with each other when things are tough/conflicted etc
      • In normal office setting we'd see this, be able to reach out to each other
      • Takes more care in the remote environment
  • Next month: Send out reminder with link to pad to spawn thinking about retro stuff in advance

Standup -- 2021.03.22

This week

  • Igor: work on integrating the typechecker
    • 100% on-board with types
    • Types are catching problems
    • Igor:
      • Would like to make todo list and merge in PRs
    • Jure:
      • Wish we had designed the work on the builder on this upfront
    • Igor:
      • I didn't know we had to do this work up front
    • Jure:
      • Type handling internally should be handled by pattern matching on arguments.
      • Envision builder as determining type structure from the syntactic structure of its arguments.
    • Igor:
      • We use builder in 3 places
        • to construct untyped
        • construct typed
        • in SMT which is not quite typed
    • Jure:
      • Issue with current approach: builder creates parallel structure, and this is only needed because typed and untyped expressions inject data after the fact.
      • If pursuing explicit type tags, we only need manual annotation in builder for named expressions.
        • For untyped we just manually pass the argument Untyped
    • Jure:
      • Suggestion for future:
        • Make a parallel structure in its own PR
        • Then refactoring PR that translates everything
      • Wants builder to be the go to way of making TLA expressions
        • Stop manually creating expressions
        • Builder is the part of the code base that allows us to write smoother types.
    • Approach to aliases
      • Way aliases are being used should be replaced with variables
      • Let's just move away from need to aliases at all
      • If we have a better way to construct expressions maybe we don't need the aliases at all.
    • Sketch for alternate architecture (Jure):
      • Builder is parameterized on the "way we handle types"
      • Two aspects of builder:
        • Construct syntax tree
        • Annotate syntax tree with types
      • Suggest builder just constructs syntax tree
        • A separate class to annotate
      • Since builder always constructs expression bottom up, we don't have any sort of full type inference to cope with.
    • Jure will write up proposal for alternate approach
    • Lesson for the future:
      • Don't commit to give talks on things that aren't in the repo yet
  • Jure: JSON ADR

Next week

  • Jure:
    • Will look at open PR for running python examples
  • Igor:
    • Merging in type checker PRs
  • Shon:
    • Tracer

Standup -- 2021.03.08

  • Josef: What's the plan to plan to the work for the Viennese grant?
    • Meeting with admin people next week: boot strapping meeting
      • Shon to schedule
        • Not at Wed. 2pm
        • Josef to go in meeting on March 18th, schedule this meeting for after that.
      • Preparation
        • Review the proposal in advance
        • Send proposal PDF to everyone
      • Agenda
        • What's been written in the proposal
        • What it implies for implementation
        • Make a roadmap, and compare with current plans

This week

  • Igor
    • Type checker integration
  • Jure
    • ADR for JSON
      • Don't currently have anyone using JSON deserialization
        • But is anyone using deserialization?
        • Depends on the serialization format.
  • Shon
    • Tracer work
      • CLosed Prototype milestone

Last week

  • Jure
    • Merged JSON formatting etc.
  • Igor
    • Tried turning off inlining for nullary operators
      • Because inlining interferes with some optimizations
      • Caused problems with cache of CHOOSE expressions
        • With the inlining off it introduces non-determinism
      • Also turned up some parser issues
        • Recursive function parsing of included instance doesn't preserve is_recursive flag.
        • Family of problems here: getting incorrect input from SANY parser
          • TLC and apalache now diverge on certain semantics.
      • Not a pressing issue
      • We'll postpone this until after the alpha release

Action items

  • Jure: open issue about parsing bug in SANY
  • Shon: to schedule a meeting in late march for Vienna grant
  • Shon: close release PR

Monthly Planning -- 2021.03.01

March

  • Igor:
    • Integrating the type checking. Slow, error prone work, but making progress.
      • It's painful to have two type checkers
        • Shon: Aren't we gearing up to have 2 checkers still, with Jure's type inference (which will include the checker)
          • Igor: These may converge.
  • Shon:
    • Packaging
      • This will be important for the Alpha
  • Jure:
    • JSON encoding etc.

Future directions

  • Alpha Release in early April
  • Better SMT encoding
    • First choice, but should depend on user input
    • But if usability is a bigger blocker, then we should focus on this
  • Translation to Scala/Python
  • Importer to our internal representation
  • Preprocessing code
    • We could try doing something like partial evaluation during, to simplify and optimize expressions, and providing the SMT encoding more opportunities.
  • Our main challenge is supporting the full scope of TLA+
  • MBT Support and integration
    • Using PBT generators for the data structures?
      • Can produce Data that you can abstract to high-level representation.
      • Then testing against the TLA predicate.
      • Can translate some part of specs to type-level, then refine with predicates for PBT?
      • Going from what we have generated to TLA space is easy than going the other way
  • Benchmarking "product"

Retro -- 2021.02.25

What went well

  • benchmarks seem to show the tool is behaving well
  • interaction with new users (zulip and github)
  • releases at regular cadence
    • seems to be improving our traffic
  • more user attention according to github stats
  • now that we have external issues and contributors, we may be disappoint expectations from external users/contributors
    • This puts psychological pressure on us to keep up and deal with the work effectively
    • Some worries about pending overload
      • Perhaps a first-responder role?
        • Only when we scale up, with bigger headcount.

What didn't go well

  • ad hoc decisions to change pretty-writing
    • Stemmed from counterexample printing
    • The change was necessary, but our handling was too improvised
    • We need to document process better and/or keep scope more focused
    • So maybe spin off followup issues rather than increasing the scope of the current work
  • Irregular JSON serialization caused problems (turned up late)
    • outdated code
    • discovered by new user

How to improve

  • Add test coverage metrics
    • Should turn up dead code
  • more unit tests, including property-based tests
    • Add PBT to ensure serialization is inverse of deserialization for JSON
  • Instead of increasing scope of work items, create followup issues and deal with them sequentially
  • Schedule a "feature audit" to make sure our CLI is sensible and well tested
  • Write a document that exposes our API
  • Better process to address new users' questions on github
  • benchmark publishing?
    • revert snapshot item
    • add docs to release and benchmark-test to explain gotchas
  • Find some way of giving appreciation to early adopters

2021.02.22 -- Standup

This week

JSON Encoding

https://github.com/informalsystems/apalache/issues/595

This structure is strange:

        "and": [
          {
            "eq": true,    <---------------!!!
            "arg": 0
          },

Something more natural would be

{"op": "and",
 "args" : [
  {"op": "eq", "args": [true, 0]}],
  ...
]
  • Shon: Can we use something like https://circe.github.io/circe/codec.html ?
    • Igor: We need to be sure that scalars "(ints and bools and stuff)" get unwrapped into the expected JSON values instead of a customized form.
    • Jure will explore this.
  • Shon: Looking back, this is a case where we would have benefited from more code review. Is this something we need to be aware of for MBT development in general? Should we be devoting cycles to reviewing MBT dev (and vice versa)?

re: Python encoding

  • Jure: Let's integrate the feedback on this, by creating a section that compares naive translation (using Range and mutable sets) with the actual encoding needed.

Bug reports

  • A few came in via Zulip last week. We're trying to prioritize them effectively.
  • This is good quality feedback, but we've some concerns about getting overhwelmed.
  • Shon: Hopefully we'll get ahead of the bugs because the software will stabalize, and if we get many more users that will also come with some contributors or exper users who can help field some of the response.

08.02.2021 -- Standup

Action items

  • Jure: Look at what TLC does with the --continue flag, and see how that format works.
  • Igor: Make sure an issue is open for TLA -> Python converter
    • Jure and Shon expressed skepticism about the value of this
  • Jure: Connect with Andrey to determine how to output

Last week

  • Jure: PR with counterexample output clenaup
    • Will address change request in followup PR.
    • Jure is having to cleanup some tech debt with PrettyWriter/PrintWriter
  • Igor: Discussion with Alexander N re: Python examples in Manual
    • He's advocating for more pragmatic Python examples.
    • The discussion is helping to refine our plans for translator from TLA to Python.
  • Shon:
    • Benchmarks are now running automatically in CI:

This week

Igor

  • Reformatted entire code base
  • Adding types as implicits PR #557
    • Jure: Does this actually save anything over just adding a map?
      • Igor:
        • Will just be a reference, won't need to look into the hash table to find your type.
        • If you store the type annotations in a hashtable, then all transformations need to creat a chain of references to expressions IDs that we'd need to trace back to get the types.
    • Jure: Gennerally worried in using implicits that we'll get bugs that are hard to see, because it'll occurr in a place we're not looking.
    • Igor: I want to gradually introduce type-aware behavior without breaking everything at once.
    • Jure: Do we have adequate tests for this change?
    • Jure: Worried we'll open up the potential for cascade of breakages

Jure

  • Andrey's transition sequence counterexample search
    • But what is the behavior of this tool supposed to be?
    • Current output: we right everything to 3 output files.
      • Do we make separate files for each counter example?
      • Shon: Why not a stream of json objects?
      • Jure: We need compatibility with TLC.
        • So in that case we have to output the format that TLC takes
      • Igor:
        • We'll dump each counterexample to a single file.
        • And create an index file that lists all of these output files.
      • Igor: Look at what TLC does with the --continue flag, and see how that format works.
    • Jure: I think the constant need to be TLC compatible is holding us back.
      • It's good in the inputs, but unnecessary in the output.
      • Igor: But outputs are important for potential integration with toolbox.
      • Shon: Could we put compatible outputs on the backlog until it's pressing?
        • Seems to agreement with this.
    • Igor: For the counteraxmple output, it's important to be able to load them in TLC and walk through them.
    • Shon: Let's make sure we prioritze Andrey's immediate needs and we can then iterate on the output for TLC compability later.
  • Finishing up pending PRs

Additional discussion items

  • Igor: Our CLI parser is non-standard.
    • E.g. can simplify passing multiple lists.
    • Let's be on the lookout for finding a good CLI parsing lib.
  • Parallel exhaustive model checking would be cool, but not a priority.

02.04.2021 -- Strategy Meeting

Action items:

  • Andrey: Add issue for "exhaustiveness" separately (Andrey) - done #542
    • Detail suggested approach for the BFS + incremental counter example report
      • Should reference #79
  • Jure: Break up the type inference integration into smaller issues
  • Igor: Send link re: TLC serialization to JSON to Andrey

This month

  • Igor:
    • Continue on type checker
    • Manual
  • Jure:
  • Shon:
    • wrapping up benchmarking in CI (hopefully this week)
    • Then stepping back for the quarter for some focused time on Tracer & PBT (for at least a couple weeks)
    • still available for code review and critical support

Discussion

  • Andrey: Prioritizing MBT support

    • "incremental bug finding": https://github.com/informalsystems/apalache/issues/79

    • Igor: revive "DFS"?

    • Andrey: No :)

    • BFS is preferable because it finds the buggy cases sooner (?)

      • Maybe Jure can work on this?

      • Need simple output

    • Why are we not prioritizing this in Feb?

      • Igor: not essential for April Alpha release

      • Need clear sense for what Andrey wants

    • Andrey:

      • I want simplest approach for exhaustive search.

      • I want one counter example per sequence.

        • Igor: So we want BFS + counter example detection.

  • Jure: need substantive feature to work on

    • Type inference integration?

    • Counterexamples? <-- Critical path to alpha release

      • https://github.com/informalsystems/apalache/issues/265

      • Improving output format

      • Track source location of errors

      • UI question or bug? UI bug.

      • Igor: Will need to write tests

        • So we'll need to cat out the contents of the counter example file that's generated in the integration test?

    • What output should this be?

    • Reference TLC to see what kind of info it reports.

    • It reports which state giving a counter example was triggerd by which action.

    • Extract spec into tree of operators that are actions.

    • Then annotate every operator with an "action" annotation.

  • Igor: what do we need for the Alpha release?

    • Type checker

    • Counterexamples work from #265

01.02.2021 -- Retro Meeting

January Retro

Went well

  • Releases automated (have released approximately weekly)
  • Got external contributor!
    • We don't know him.
    • Making very small doc contributions to typos etc.
  • Published nice looking docs
  • 33 twitter followers :)
    • Igor has also started requesting upvotes/downvotes on feature issues. Good way to get feedback
  • more focus on features
    • (aside from some distractions)
  • we have scalafmt! No fighting over spaces :-)
  • there is constant traffic on github -- the effect of releases
    • (igor) this is new
  • metrics on dev velocity are up (ito of commits/loc)
  • (igor) scoping issues much better now

Didn't go well

  • external issues cause deviation from the plan

  • execution statistics does not show up yet

    • indicating that people haven't opted in and/or aren't using it
    • (Andrey) we probably need to provide some incentive, like automate bug reports but only if people opt in to stats sharing.

  • (shon) didn't close most of my issues (including the benchmarks)

    • infra is painful in general?

    • Maven is rough?

  • (shon) getting tired of infra :/

    • breaks will be coming

  • Didn't close out our milestone issues

    • this is just part of learning our cadence
    • should get better over time
    • getting visibility on our progress is the main thing, and that's working!

  • emoji's in the new docs :(

How to improve

  • start breaking down conceptual issues, to refactor into smaller tasks
  • find a way of tracking small contributors/acknowledgements (not necessarily in the license)
  • support emojis in docs
  • integrate stats sharing with automated bug reports
  • maybe SBT would make builds nicer?
    • but there's a good amount of risk here too
    • we can consider this after the Alpha release

Arrange next month's milestone

  • Andre: wants some MBT issues in Feb
    • Exhaustive checking
    • JSON serialization of all key data
    • Will discuss in more detail on Thursday
  • Review outstanding January issues
    • Backlog or pull into Feb (pulled everything into Feb)

Topics

  • Type checker is renamed to "Snowcat"
  • We'll do strategy planning on Thursday

18.01.2021 -- Standup

Last week

  • Jure: Working on manual on assignments and actions
  • Igor: Landing multi-core + manual
  • Shon: Release pipeline

Topics

  • Igor: We'll need to run integration tests with our different different model checkers
    • Shon: Let's make sure those are exposed via feature flags we can toggle from the CLI, via environment variables, then we can just run the integration tests in a build matrix with the different env-vars set.
  • Andrey: Needs #191 and #79 for MBT.
    • How urgent? Not currently blocking, but the promise of MBT is somewhat stifled until these are landed.
    • Igor: We'll plan to get to these in Feb.
  • Igor: Traffic to our repo is up.

Action items

  • (Igor) Open issue for integration test matrix
  • (Shon) New release with breaking fix by EOD
  • (Jure) Add changelog entry for breaking fix

This week

  • Jure: Bugfixes and refactoring
  • Igor: Sequential model checker + type checker
  • Shon: Finish release pipeline, then focus on benchmarks

04.01.2021 -- Strategy Meeting

Agenda (Igor):

  • intro Vitor
  • post-holiday chat
  • releases:
    • weekly releases
    • two editions: community (feedback) and privacy (no feedback)
    • how to highlight major releases?
  • January iteration:
    • what shall we include?
    • what are the high-level goals?
  • document the process

10.12.2020 -- Strategy Meeting

Action items

  • Move meetings notes to the wiki (@shonfeder)
  • Start an Apalache twitter account (@shonfeder)
    • We decided to communicate through the informal account for now
  • Add PR template to remind contributors to...
    • add tests
    • add documentation
    • update release notes
  • Implement a weekly release cadence (with stable releases cut whenever it makes sense due to feature-set)
  • Plan for an alpha quality release for March
  • Write up plans for dev process going forward:
  • Schedule monthly strategy meeting (invite Andrey)

Discussion

  • Meetings:
    • Be more disciplined about holding weekly stand-ups
    • Hold monthly strategy meetings
    • Keep meetings notes in github wiki
  • Dev process
    • Reduce WIP and focus on finishing features in progress before starting new work items.
      • Let's keep each other accountable on this
    • Let's break up issues into smaller pieces when we can
      • Will help lead to smaller PRs
      • Will help reduce WIP
    • We need regular backlog grooming
      • Will do async before monthly strategy meetings
    • Only have two milestones active at a time -- we'll use these to track our velocity:
      • One for the work currently in process during the month
      • One for the work planned for next month
  • Releases
    • Process
      • Weekly releases
      • Increment the version number to fit the content of the release
    • Aim for an alpha quality release in April
      • Stable type checker
      • Assignments fixed
      • More extensive testing
      • Fill in gaps in manual
  • Work items
    • Try a non-smt based type type inference? (@Kukovec)
  • Outreach
    • Start tweeting info and updates

Agenda

Please add your ideas!

Igor:

  • What we do well:

  • tactical planning: github issues, bugfixes

  • peer-reviewing

  • the infrastructure has improved a lot thanks to @shonfeder

  • research prototypes

  • What we do not do well (shame on me):

  • no well-defined strategic planning (hey, it was a research project!)

  • our milestones are more like features:

    • the deadlines in the milestones are never met (because our milestones are not milestones)
    • due to the nature of our project, many features need 1-2 months of work
    • there are a lot of interdependencies between different features, so our milestones are creeping
    • see the new features

  • new features are hard to merge, sometimes, breaking the builds

  • need for more systematic and automatic testing of new features: they should come with unit tests and integration tests

  • We do "move fast and break things", but we never know when the tool is stable enough to cut a relase

  • Hard to cut a release, as unstable accumulates the code of the partially implemented features

  • As we are doing more engineering now, we have to define and codify our engineering process:

  • we need to formulate (and document) a common understanding of:

    • how we organize large chunks of development (merely introducing a milestone does not help)
    • how we test new features
    • how we check test coverage of the new features
    • how we test bugfixes and collect regression tests
    • how we merge new features without stepping on one another's toes
    • how we integrate all above in the github infrastructure

  • our project has a heavy research component:

    • the techniques are documented in the research papers
    • as a result, it is hard to understand several modules by just reading the code
    • new techniques are first implemented as research prototypes and are made stable with time

  • we should pick the best practices from the processes that suit our project. The planning-oriented processes seem to be very heavy on form-filling, e.g., TSP and the introduction in TSP. Agile processes seem to be to fragile for developing a compiler-like tool. We should pick the best practices from both. For instance, I am developing new code with TDD.

  • we should extract useful HOWTOs from the known processes: planning, structuring development cycles (features, milestones), doing meetings, measuring enchancements (e.g., in unit and integration tests).

  • we should avoid heavy bureaucracy, e.g., we should not waste our time on filling time sheets (though it is a good idea to personally track your time).

  • we should avoid writing a survey on all available development processes.

Clone this wiki locally