Theorem proverlar g'oyasi kechagina paydo bo'lib qolgan narsa emas.

Man bilganim Automath project eng birinchi teorem proverlardan batafsil: https://automath.win.tue.nl/

Umuman olganda bu mavzular asosida juda ko'plab ishlar qilib kelinyabti. Theorem proverlar katta tarixga ega bo'lsada haligacha juda aktiv izlanishlar qilib kelinyotgan sohalardan.

Umuman olganda bu sohalar ham raqamli dunyoning bir ustuni desak bo'ladi. Mavzular atrofida juda ham ko'p qiziq tadqiqotlar mavjud. Hozirgacha SAT solverlar o'rtasida raqobat bor, kim tez ishlaydigan SAT solver qilishga musobaqalashadi: https://satcompetition.github.io/

muhim bo'lgan deyarli hamma crashlar yeg'ilyabti endi :)

bunisi surpriz bo'ldi macosda

Hullas 3ta devaysim xozir actual.

1. PC - Ram ECC bo'lmaganiga memory corruptionlar handle qilinmaydi.
2. Laptop Nixos - HDMI ishlamaydi hamma narsa qilib ko'rganman faqat Type-C bilan monitor ulay olaman baxtimga.
3. Macos - Kayfiyati yaxshi bo'lasa ishlaydi.

Bu narsalar shunchalik kulgiliki - man umrimda biror muammosiz laptop yoki telefon ishlatib ko'rmaganman.

Oldingi devayslarimda ham muammolar bor edi. Manimcha yangilarida ham muammolar chiqadi.

Manam video qilsamikan.

One day of my life deb.

ORB stack nixos machineda ishlata oldim vanihoyat.

Macos uchun parallels ishlatmasdan ham nix yengil nix machine run qilsa bo'lar ekan.

Load deyarli sezilmaydi albatta build paytida ko'proq ram yeyabti ammo bu chepuxa muhimi build bo'lyabti.

Hullas ORB stackda unstable nixos run qivordim va baxtliman.

Tez orada configimni ham ulashib qo'yaman.

Conflict-free Replicated Data Type (CRDT)

Introduction: https://mattweidner.com/2023/09/26/crdt-survey-1.html

More resources: https://crdt.tech/resources

Where to Store PID Files for User-Run Daemons: Best Practices & Alternatives to /tmp

https://linuxvox.com/blog/storing-pid-file-for-a-daemon-run-as-user/

Dunyoda sodir bo'layotgan voqealar huddi videoni 8x speedga qo'yganga o'xshaydi.

Ammo manashu voqealikda taraflarga bo'linib olib bir birini go'shtini yeyotganlar hammadan ko'proq zararda bo'lsa kerak. Vaziyatdan foydalanolmayabsizmi ? Demak kamroq zarar ko'rish kerak.

Aytgancha bir servercha qilmaymizmi generals uchun :)

Verification codeni 1 daqiqadan kegin yuborganlarga nima deyish kerak ?

Orb stack machine juda ham zo'r ishlayabti macosda.

Bemalol nixos ishlatsa bo'ladi, bu yerda config:

https://github.com/lambdajon/confs/tree/main/nixos/orb

Faqat shu desktop qo'ymasdan ishlatyabman, yomon emas.

Configim juda bordak bo'lib ketgan o'zi, shu bahona sekin sekin desktop, server va nix-darwinlarni tog'irlab olaman.

Umuman olganda manda nixos muhitlar juda ko'payib boryabti.

Shularni sekin sekin tartiblab joy koyiga keltirish kerak. Main devayslarim configlari ~37GB bo'lgan tag'inam bazi narsalar qo'shilmagan.

Macosda qiziq muammo mavjud.

Masalan xozir manda N ta servis ishlayabti deylik va memory 60% turibti.

Ammo macbook zaryadi o'chib qoldi va qayta zaryadga qo'yib yoqdim albatta snapshotlardan recover qilinadi va hammasi qayta tiklanadi.

Tizim o'chib yongani bilan hechnima kill bo'lib ketmaydi. Ammo qiziq tomoni shundaki manashu voqeadan kegin macos 80-90% memory sarflashi mumkin.

Bu yerda potensial sabablar ko'p, lekin aynan ARM processorlarli macbooklarda manashunaqa narsa ko'p kuzatiladi.

Bu masalada aniq texnik argumentlarga ega emasman, lekin qiziq holataq chunki bu narsani doyim kuzatganman.

Bizni crash detector aynan bazi caselarni detect qila boshladi, masalan coredumplar.

Ammo servislar fail bo'lgani kabi masalalarga yozgan handlerlarimiz kutganimizdek ishlamadi, kegin journaldan hamma datani ovolib shu bilan ishlashni uni analiz qilishni boshladim.

Kegin kutilmagan narsani ko'rdim, ishlab turgan nixos based distrodagi journalda man kutganimdan ham ko'proq fieldlar bor ekan. Bunisi yetarlicha surpriz bo'ldi sababi o'ylaganimdan juda ko'p va turli devayslarda turlicha fieldlar bor.

Birnechta devayslardan dataset to'plab ularga parser yozdim, kegin bazi narsalarni analiz qilib ko'rdim masalan manashu journalda mavjud barcha fieldlar...

Albatta parserlar bilan birnechta narsalarni analiz qildim, ammo savollar ko'paygan sayin muammolar ham ko'paydi.

1. Har bir ideyani tekshirgani yoki savolga javob topgani alohida code yozish kerak.
2. Bazi narsalar natijasini olish uchun yoziladigan kodlar optimal bo'lmagani uchun uzoq kutish kerak ayniqsa 1GB log faylar bo'lsa.

Qisqasi, qarsasam uje DB yozib qo'yabman.

Ha, kegin journaldan olingan dumplar contentlarini tog'ri mongodbga yozdim. Mongodbdab schema generate qivolib bazi fieldlarga indexlarni tiqdim bunga alohida sodda index generator yozvordim.

Shu bilan xozir 1mln documentlik journalarni dbdan bemalol aggregate qilolyabman, bu narsa esa asosan turli edge caselar, turlicha catch senariylar qilish uchun kerak.

Masalan xozir systemd qanday dasturlani manage qilgan ?
Qaysi dasturlarda muammolar sodir bo'lgan ?
Kernel scopeda qanday muammolar sodir bo'lgan ?
Falon dasturda errorlar sodir bo'lganmi ?

Hullas manashunaqa savollarga ancha tez javob olyabman.

Endi ushbu savollar problem detection case bo'lib xizmat qiladi codega o'girilsa bo'lgani ))

Juda sodda lekin juda effektiv.

Haa do'stlar uje githubni ham yoshi o'tib qarib qoldi.

I mean rust but...

Hackage ochvolib nega manga crates emas hackage ochib berdi deb o'ylanib o'tiribman.