silly_giraffe

I want to say that I am continually impressed at your long-term vision and commitment you have taken to the Oil project. Your posts are a treat to read, and the care you have given to the problem is appreciated. We need to stop paving cow-paths, and discard historical baggage if we are ever going to build robust systems.

The documentation and API quirks of z3 also led me down some performance sinks before I was able to tackle the larger models. Not a Z3/SMT expert, but what worked for me was to model every time tick as the sum of all tasks that could be performed at that instant. Set a constraint on each tick that sets the sum of these tasks to be <= P. Add the book-keeping on the task-job relationships and that was it.

Using the Python bindings, the biggest performance impact I discovered was ensuring that my jobs and tasks were represented as z3.Bool and not z3.Int (requiring a roundabout way to do a summation on z3.Bools). Something like:

  tasks_this_tick = [(z3.Bool(task_id), 1) for task_id in current_tasks]
  model.add(z3.PbLe(tasks_this_tick, max_tasks_per_tick + 1)

I have used the Z3 solver(https://github.com/Z3Prover/z3) to optimize a job scheduling problem. Roughly, I have ~20k jobs, defined by N tasks (~1-50). A job is complete only if M tasks (typically 2-3) per job are done. Every task takes some variable amount of time to complete and can only be run during specific windows. Given the equipment can only perform P tasks in parallel, what is the optimal configuration of tasks (~500k) that will allow us to complete the most jobs?

The search space for this problem is enormous, but Z3 will produce an impressive result within a few minutes.

While still an early project, I am keeping my eye on the Tectonic(https://github.com/tectonic-typesetting/tectonic) project. A re-write of the core Xetex engine in Rust with a focus on many quality of life improvements - useful error messages, UTF8 always, less line noise during build, eliminating the intermediate files, etc.

>same stuff within the standard library, like list.sort() and sorted(list)

Those have different use cases. `sorted` is for situations where you would use a list comprehension and immediately consume the result vs `.sort` where you need the iterable sorted for future use.

As a quick scribble, you can do something like the following to sort random numbers in a single line:

  result = sorted(random.random() for x in range(10))

From your Medium post:

  def list_sort(arr):
    return arr.sort()

  def sorted_builtin(arr):
    return sorted(arr)

Only the `sorted_builtin` function returns the array, `list_sort` returns None. The `list_sort` function would have to become:

  def list_sort(arr):
    arr.sort()
    return arr

Edit: goofed the formatting

I have read through the first few chapters now and it is brilliant. The author uses excellent examples without ceremony that makes the topic far more approachable than I found it in school.

Thanks for making this resource available and giving it some exposure.

If I could add a personal number three to your list: most robots are far from robust. Running a robot becomes a full time job and require a dedicated guru to maintain it. The activation energy to use the equipment means that you must be desperate enough to deal with the pain rather than do the job manually.

SQLite will sell you a perpetual license if you need it.

While I completely agree that there are Unix idioms that could go by the wayside, the team is already taking on an enormous project. Reinventing standard practices at the same time (and the ridiculous bike shedding that would ensue) seems like an even more impossible task.

SQLite can handle a lot more than people think. The SQLite website uses it for production (https://www.sqlite.org/whentouse.html)

Except for us crazy individuals that need the computer on for uninterrupted data processing. I have Windows only software that can take two weeks to complete a dataset. There is no intermediate data backup, so if the job is killed, I have to start over. My only reliable option has been to keep it off the network.