2,738,281 events, 1,404,592 push events, 2,192,793 commit messages, 164,195,019 characters
Add: another quote for the file. Also had a crazy idea that the install script should be turned into a Makefile. I hate writing Makefiles! After struggling with it for a couple hours I just put it away and I should delete it but can't bring myself to it.
"9:15am. I've been chilling for a bit. Let me do it some more and I will start. Today I will start work on the multi-file server. I'll first get that out of the way after that comes the package server. After I have those two, I'll be able to
9:45am. Let me start.
9:50am. I am really shocked just how viable solo mage builds are in Baldur's Gate. My eyes have been opened. This experience has been wonderful. Before starting this I thought that not having numbers would be a significant disadvantage, but there are endless tactical advantages to this. In addition to the increased XP allowing me to cast far higher level spells, I keep getting good equipment like boots of speed that really shine on a solo character.
I am going to continue it later today. But now let me focus on programming.
I have the whole day ahead of me and I can do great things with it.
9:55am. If days like this could continue things would not be so bad, but as a human I know that my lifespan is limited.
So I need to put some effort towards my actual goals.
10am.
type TypecheckerFiles<'a> =
| File of name: string * stream: 'a Stream
| Dir of name: string * 'a TypecheckerFilesLet me start with this. I've been thinking about this yesterday.
let multi_file_manager (req : ParserRes TypecheckerFiles Stream) =
()Yeah, the function needs to take in input like this. But this is too complex.
let multi_file_manager (req : ParserRes TypecheckerFiles) =
()I should start with just the regular inputs. Once I have this I will be able to compose this.
let typechecker package_id module_id (req : ParserRes Stream) : TypecheckerRes Stream =Let's see, the output for the multi_file_manager should then be...
let multi_file_manager package_id module_id (req : ParserRes TypecheckerFiles): TypecheckerRes TypecheckerFiles =I of course need the two ids.
Though I've thought about it in depth yesterday, there is a really a lot of stuff that goes into these servers. I'll have to deal with them step by step.
10:25am. Had to take a short break. Let me keep going.
Yeah, in the finished product there are just so many damn things to deal with it.
Right now I have all the pieces in my head, and there aren't anymore unresolved issue that give me anxiety.
10:30am. The amount of useful work I've done so far is quite scary. I've come quite far, both in my understanding of concurrency and language design at large. It is an enormous pile of experience that I've acquired.
I need to go even further.
let multi_file_manager package_id module_id (req : ParserRes TypecheckerFiles): TypecheckerRes TypecheckerFiles =
failwith "TODO"Yeah, let me focus on this. One of the things the completed version should have is optional inputs, but for now let me ignore it. I should be able to redesign the completed thing to allow partiality. But now building up the skeleton should take precedence.
The reason why I want optional inputs is so that the later nodes freeze their processing and wait, while the previous nodes do their work. This is a really smart thing to do, and I should do it, but right now having that consideration on my mind is just a burden.
10:35am. The main issue facing me now is taking the big, top-down design that I have in my head and slicing it into actual steps. I must make sure that none of the steps are too large for me to take. Once I do that, then any task becomes possible.
type TypecheckerFiles<'a> =
| TCFile of name: string * stream: 'a Stream
| TCDir of name: string * 'a TypecheckerFiles
let multi_file_pipe package_id module_id (req : ParserRes TypecheckerFiles): TypecheckerRes TypecheckerFiles =
failwith "TODO"Yeah, things are too hard, so for now let me just focus on making this particular function. I won't even do the diffing here. This will just be a part of the larger server.
let multi_file_tc _ = failwith "TODO"
let multi_file_pipe package_id module_id (env : Infer.TopEnv) (req : ParserRes TypecheckerFiles): TypecheckerRes TypecheckerFiles = failwith "TODO"Let me just pass in the env as if it were a regular argument.
Servers really are a huge pain in the ass. Rebuilding everything would be easier.
...Hmmmm...
I need to think about switches. During my Rx adventure, I got familiar with the switch combinator there. I have a need for the same thing here.
One thing that is particularly hard with the Hopac servers is that it is difficult to shut them down. They are more 'live' than observables, but that has its own disadvantages of forcing me to write extra subscription unsubscription code.
I'll have to do it. There is no choice. Just focus on this.
10:50am.
type TypecheckerRes = (Bundle * Infer.InferResult * Infer.TopEnv) PersistentVector * boolI am trying to get into it. This thing is such a problematic, troublesome thing. In my mind I only have eyes on the ideal form because there is no room for much else there.
But now what will I do with Bundle and InferResult here. I don't need that shit.
What I really envisioned and what was the great breathrough is how to compose TopEnv.
10:55am. That is what I should focus on.
For this initial run, let me just ignore dealing with hovers and errors much like optional inputs. Right now I should be focusing on stitching everything together. I'll deal with hovers and errors in due time when I make the general framework surrounding them.
11am. It is really more difficult to focus in the concurrent regime isn't it? I never thought that changing the domain would be affecting me mentally to this degree. I think about one problem, and then I start thinking about another one.
I actually have to force myself to be on the ball and think less about some things.
I find this very challenging.
11:05am. Now I am thinking again how to deal with the prepass. There is just so much to keep track of that I keep forgetting key things.
I am thinking about synchronization issues that would come with sampling, and optional inputs really are the solution to this problem. I keep running it in my head without them and it does not work. Optional inputs are vital.
12:05pm. It really was my intention to do some programming in the morning, but in the last hour I've had waves of inspiration come to me.
A large amount of my anxiety over the compilation pipeline is about managing these servers. When the time comes to rebuild them, I'll have to shut them down and start them again, and it is just such a painful thing to deal with.
I keep thinking of this in terms of data flow, but these servers always force me off my game and I have to essentially emulate the higher level model in my head.
12:10pm. A though came to me that what if instead of eager servers and eager streams, I imagined all of this in terms of lazy streams.
I decided to try to elaborate this idea and it all came to me. Everything.
This is not the first time I had this idea, but previously I was too inexperience with Hopac to make anything of it. It is only now that I understand its primitives well enough to make the connections.
As an experiment, I am going to see if keepPreceding1 is lazy. I had this hypothesis before, and I reasoned out that it must be eager because I could not see how it could be implemented in a lazy manner, but with my newest insights I see that this would very well possible.
12:15pm. Well, it might be eager, in fact it probably is for the sake of space efficiency, but I shuold test this. I might be surprised at the result.
At any rate, I am going to scrap everything and start from scratch once more. Doing a lazy implementation of the compilation pipeline would just be much easier than dealing with eager servers. This insight is on par with how to do the concurrent depth first traversal that I had a while ago.
Communicating servers are just so troublesome to manage. They are so hard to reason about.
All this time I knew that Hopac streams were intended to be lazy, but I did not know what that really meant. I think I do now. I am going to have to play with it.
I see now that there are much better ways of making use of streams than treating them as observables and pumping them with Src.value."
printk: Dont print init related logs
Due to some fuckups from ROM side now the userspace spams my dmesg with following logs so ignore all init messages once for all This is annoying as hell.
init: Could not find '[email protected]::ICrypto/default' for ctl.interface_start
Signed-off-by: wimbiyoas [email protected]
UICHKOUT-666 stretch the OverrideModal's height (#551)
How gross is this hack? Let me count the ways.
It's gross by using breaks to set the height
So <Datepicker> will render full, in-sight
Instead of clipping first or final days.
usePortal pops it out, but sets its place
From modal's y position, hardly right,
And so ensues a render offset fight.
It's gross but so so simple, earning praise?
It's gross and leaves a rake to later bruise
Oneself by all who place a month with faith
That it will show, unclipp'd, no edge to lose.
You'll fix the stripes-component? Hold my breath
I'll not. There, CSS collects its dues.
You love my gross fix. It's simple. Like death.
Refs UICHKOUT-666
Stupid 302 return for no real fuckin reason once I added my wp-config file. Deal with this shit tomorrow
Etc Branch Mono-commit
To eliminate spurious merge commits that keep showing up, this combines all the commits from the prototyping branch frozen at #244 into a single changeset.
added sparse tuples in the type grammar
wip: translator from TlaEx to simple typed lambda calculus for type checking
translating recursive functions
translating control operators
translating action operators
translating sequence operators
translating temporal operators
translating LET-IN
type unification for TlaType1
using integers instead of strings in VarT1
using the type parser in TestUnifier, to increase readability
refactoring tests, to make them comprehensible
unification for lists of pairs
refactored the STC language (which will become ETC soon)
the first working type checker for ETC, needs refactoring and more tests
moving the ETC related classes to etc
name change
refactoring: introduced ExactRef and BlameRef
cycle detection in unification
renaming conflicting variables
testing the type checker with the most exciting expressions, bugfix in recursion
refactoring: extracted onTypeError
handling type annotations in Typing
all methods in EtcBuilder are made protected
handling empty sets and sequences
fixed TLA_PATH in apalache-mc
added typecheck command
allowing for polymorphic arguments
better type errors
fixed unification against uninterpreted types
first integration test for the type checker
bugfix for a one-argument function
fixed the off-by-one error in tuples
a sparse tuple unified with a tuple becomes a tuple
fixed unification for sparse tuples and tuples once again
handling the advanced syntax in set comprehensions and function definitions
friendlier error reporting
forcing the type from a nullary type annotation, needed for <<1, 2>>
bugfix: translation for CASE..OTHER
friendlier messages
the typed version of game of life
computing the transitive closure when doing unification (how did I miss that?)
the typed version of Missionaries and Cannibals
a few changes in the output
a quick bugfix in the importer when type-checking Paxos
added unbounded CHOOSE
disabled polymorphism for user-defined operators, as it is delaying errors
generating unique type variables instead of fixed ones
fixed variable unification
renaming variables in annotations
the new constraint-based type checker
refactoring: using var pool instead of integer indices
debugging the new type checker
more debugging
bugfixing the unifier. Needs more eyes.
propagating parameter types for better inference
still debugging
the examples that go through (some are type incorrect)
two more examples
updated the annotation syntax
Drop outdated changes
Remove EtcTypeChecker
Superseded by EtcTypeChecker2, as noted by @konnov at apalache-mc/apalache#264 (comment)
Restore erroneously removed TestEtcTypeChecker
Fix STC -> Etc
Remove duplicate code bits
Remove lingering STC refeferences
Rename map attribute to context
This prevents confusing name clashes like map.toSeq.map where the
first map refers to an instance of Map[Int, TlaType1] and the second
to Seq's' map attribute.
Wildcard pattern match in Substitution.md
This ensures that exhaustiveness checking will warn us if we add some new type in the future but forget to update it here, it also allows us to promote the documenting comment into code.
Rename another map to context
Fix map -> context in TypeUnifier
Remove depricated method
Simplify TypeUnifier insert logic
I think this reads more straightforwardly tho I suspect this may be subjective. I also think that this change eliminates some redundant logic from the case analysis in the main unification method, but I could be mistaken. Tho I'm encouraged that the tests are passing.
@konnov, let me know if you find this harder to follow then the initial implementation.
Clean up comment indentation
Clean up manual maps
Add missing newline
Update tla-types/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/TypeUnifier.scala
Co-authored-by: Igor Konnov [email protected]
Ensure solution is always reset
As per apalache-mc/apalache#294 (comment)
Rework computeOptions method into computeFields
This renames the method, so that it has a more specific name reflecting its use (as per apalache-mc/apalache#294 (comment)) and, in the process, it refactors out some common logic between the two sites of use.
Apply scalafmt
Report which type assumption conjuct is invalid
Refactor out literal to type mapping
As per @konnov's TODO
Commit scalafmt config
Document the unary apply method
Use varPool instead of hard-coded types var
Simplify record validation
Use simple structural matching instead of arithmetic. This change
also lets us validate the args in a single pass, rather than two
separate invocations of zipWithIndex.
It actually increases the loc, but that's due to more robust error handling and the addition of unit tests to cover an unhappy path.
Clean up funDef case
Mostly swapping arithmetic check to pattern matching and case analysis. Improves self-documentation and makes logic more concise (imho).
Suggestions to TlaFunOper.except translation
This change proposes:
- Structural reasoning over arithmetic
- Improves self-documentation (e.g., with defining predicates for accessor tests and using those to self document at the call site)
- Lazy vals to avoid unnecessary computations of mutually exclusive values
- Reuse of the a1 variable for the seqType. Because we are producing a sum type, the type variable scoping does not require a fresh variable fore each disjunct. Reusing the a1 variable used in the function type alternative produces more regular and consistent type variable naming.
Refactor mkApp helper
This renames the helper so that it doesn't shadow the original function (this shadowing was leading to confusion for this reader :)), and it makes the helper a closure that includes the exact ref id, so that needn't be supplied every time.
It also adds a temporary variable so we only need to construct the ExactRef once.
Remove nextVarNum
Remove outdated TODO
Don't allow for impl or equiv with > 2 args
Make catchall expression raise
To improve safety and ability to identify weird edge cases.
Use TlaOpe.deinterleave
Combine stutter and nostutter cases
Add: קיץ ערן צור עד שתעזוב ריטה ואני שר שלומי שבת Paul Simon 50 Ways to Leave Your Lover ABXtWqmArUU Aerosmith Cryin' qfNmyxV2Ncw The Marmalade Reflections Of My Life zqUDRkO93DA
Convert: Creep - Radiohead Can't Help Falling In Love - Elvis Presley Karma Police - Radiohead Simon & Garfunkel - Bridge Over Troubled Water David Bowie – Life On Mars? שיר תשרי
I take back my take back of my sperging. this retard unironcally pretends his shit is standard by throwing it in std::, uses previous hashes to seed new states of an algorithm that should have predicable results, and doesn't know how to consume bytes given a buffer type, template generic pointer, and a count. i shouldn't have to baby a dipshit who is selling c++ books on how not to be a fucking dipshit.
I take back my take back of my sperging. this retard unironcally pretends his shit is standard by throwing it in std::, uses previous hashes as salt as a namespacing mechanism, and doesn't know how to consume bytes given a buffer type, template generic pointer, and a count. i shouldn't have to baby a dipshit who is selling c++ books on how not to be a fucking dipshit.