V programovacím jazyce Go naprogramovaná webová aplikace pro spolupráci na zdrojových kódech pomocí gitu Gitea (Wikipedie) byla vydána v nové verzi 1.26.0. Přehled novinek v příspěvku na blogu.
Ve středu 29. dubna 2026 se v pražské kanceláři SUSE v Karlíně uskuteční 7. Mobile Linux Hackday, komunitní setkání zaměřené na Linux na mobilních zařízeních, kernelový vývoj i uživatelský prostor. Akce proběhne od 10:00 do večerních hodin. Hackday je určen všem zájemcům o praktickou práci s Linuxem na telefonech. Zaměří se na vývoj aplikací v userspace, například bankovní aplikace, zpracování obrazu z kamery nebo práci s NFC, i na úpravy
… více »LilyPond (Wikipedie) , tj. multiplatformní svobodný software určený pro sazbu notových zápisů, byl vydán ve verzi 2.26.0. Přehled novinek v aktualizované dokumentaci.
Byla vydána nová verze 11.0.0 otevřeného emulátoru procesorů a virtualizačního nástroje QEMU (Wikipedie). Přispělo 237 vývojářů. Provedeno bylo více než 2 500 commitů. Přehled úprav a nových vlastností v seznamu změn.
Společnost SpaceX amerického miliardáře Elona Muska oznámila, že si zajistila opci buď na akvizici startupu Cursor za 60 miliard dolarů (přes 1,2 bilionu Kč) do konce letošního roku, nebo na zaplacení deseti miliard dolarů za nové partnerství s touto firmou zabývající se generováním kódů. SpaceX se dále prosazuje na lukrativním trhu s vývojářskými nástroji pro umělou inteligenci (AI). Cursor, startup zabývající se prodejem modelů AI pro
… více »Díky AI modelu Claude Mythos Preview od společnost Anthropic bylo ve Firefoxu nalezeno a opraveno 271 zranitelností.
Byla vydána nová verze 2.54.0 distribuovaného systému správy verzí Git. Přispělo 137 vývojářů, z toho 66 nových. Přehled novinek v příspěvku na blogu GitHubu a v poznámkách k vydání.
Grafana (Wikipedie), tj. open source nástroj pro vizualizaci různých metrik a s ní související dotazování, upozorňování a lepší porozumění, byla vydána ve verzi 13.0. Přehled novinek v aktualizované dokumentaci a na YouTube. Stalo se tak na konferenci GrafanaCON 2026.
Na YouTube proběhl Framework [ Next Gen ] Event 2026. Společnost Framework představila nový Framework Laptop 13 Pro, vylepšení Framework Laptopu 16 a OCuLink Dev Kit pro připojení vysoce výkonných periferií jako jsou eGPU a bezdrátovou klávesnici s integrovaným touchpadem Framework Wireless Touchpad Keyboard.
Byl vydán Mozilla Firefox 150.0. Přehled novinek v poznámkách k vydání a poznámkách k vydání pro vývojáře. Řešeny jsou rovněž bezpečnostní chyby. Nový Firefox 150 bude brzy k dispozici také na Flathubu a Snapcraftu.
17.2.2013 20:42
Bystroushaak | skóre: 36
| blog: Bystroushaakův blog
| Praha
Bez lidske inteligence si nemuze poradit ani s takovou trivialitou jako je treba odvozeni funkce (operatoru) nerovnosti:
AbcLinuxu.cz
ITBiz.cz
HDmag.cz
AbcPráce.cz-- nejprve operator ekvivalence
(==) :: Eq a => a -> a -> Bool
-- nerovnost ?
(/=) ? Eq a => a -> a -> Bool
-- error: cannot infer
-- musi natukat clovek
x /= y == not (x == y)
-- a je to :)
x /= y = not (x == y)Bez lidske inteligence si nemuze poradit ani s takovou trivialitou jako je treba odvozeni funkce (operatoru) nerovnosti:
Docela mě překvapuje, že to nevrátí třeba x /= y = True.
Příkaz Auto zvládne doplnit i složitější výrazy. Například return a bind pro stavovou monádu doplní takto:
record Pair (A B : Set) : Set where
constructor _,_
field
proj₁ : A
proj₂ : B
record State (S A : Set) : Set where
constructor state
field
runState : S → Pair S A
-- vygenerovane prikazem Auto
return : {S A : Set} → A → State S A
return x = state (λ z → z , x)
-- vygenerovane prikazem Auto (a spatne)
bind : {S A B : Set} → State S A → (A → State S B) → State S B
bind m f = state
(λ z →
z ,
Pair.proj₂
(State.runState (f (Pair.proj₂ (State.runState m z))) z))
bind je bohužel špatně – typ totiž nezakazuje použití původního stavu. Když ale umožním, aby se typ stavu měnil (pak už to není monáda), tak Auto vygeneruje již korektní definici i pro bind:
record IState (S₁ S₂ A : Set) : Set where
constructor state
field
runState : S₁ → Pair S₂ A
-- vygenerovane prikazem Auto
ibind : {S₁ S₂ S₃ A B : Set} → IState S₁ S₂ A → (A → IState S₂ S₃ B) → IState S₁ S₃ B
ibind m f = state
(λ z →
Pair.proj₁
(IState.runState (f (Pair.proj₂ (IState.runState m z)))
(Pair.proj₁ (IState.runState m z)))
,
Pair.proj₂
(IState.runState (f (Pair.proj₂ (IState.runState m z)))
(Pair.proj₁ (IState.runState m z))))
Nicméně perfektní to není – některé výrazy se tam zbytečně opakují, člověk by napsal:
-- napsane clovekem
ibind' : {S₁ S₂ S₃ A B : Set} → IState S₁ S₂ A → (A → IState S₂ S₃ B) → IState S₁ S₃ B
ibind' m f = state
(λ st₁ →
let (st₂ , a) = IState.runState m st₁
in IState.runState (f a) st₂)
IMHO to ale moc prakticky neni.Hodí se to v důkazech. Tam potřebuji najít term s daným typem a už příliš nezáleží na tom, jak ten term vypadá.
18.2.2013 13:38
coder | skóre: 4
| blog: lINUKS
18.2.2013 21:00
Josef Kufner | skóre: 70
19.2.2013 15:28
coder | skóre: 4
| blog: lINUKS
Bez Vimu si jiz nedokazi predstavit svuj zivot 
Ale ten Emacs ma spousty zajimavych funkci a doplnku, ktere bych rad pouzival a ve svete vimu jsou nedokonale imitovane. Napr. org mod a velmi kvalitni integrace REPLu funkcionalnich jazyku. No uvidim, treba se nekdy hacknu.
Hm, moc tomu nerozumim
Máte nějaký konkrétní dotaz, třeba bych mohl pomoci?
Mně se na Agdě a podobných jazycích líbí minimalističnost kombinovaná se silou typového systému. Naopak mi vadí absence aktuální definice jazyka – bylo by super, kdyby někdo zpracoval definici na úrovni Standard ML (viz stará verze: The Definition of Standard ML - Version 2).
Hlavní využití příkazu Auto je při hledání důkazů – tam totiž jde pouze o nalezení termu s odpovídajícím typem a je jedno, jak ten term vypadá. Je tohle odpověď na vaši otázku?
int f(int a, int b)a editor me k tomu doplnil:
{
return a + b;
}
i kdyz jsem mohl chtit odcitani, nasobeni, nebo neco slozitejsiho?
i kdyz jsem mohl chtit odcitani, nasobeni, nebo neco slozitejsiho?
Přesně tak. Například, když chci odčítání a použiji typ
binop₁ : ℕ → ℕ → ℕ
tak dostanu
binop₁ a b = b
což není odčítání. Musím tedy upřesnit typ:
binop₂ : (x : ℕ) → (y : ℕ) → Pair ℕ (minus_pred x y)
Místo pouhého čísla vracím dvojici. První prvek dvojice je číslo a druhý prvek je důkaz, že první prvek je rozdíl x a y. Odečítání definuji následovně:
_∸_ : ℕ → ℕ → ℕ m ∸ zero = m zero ∸ _ = zero suc m ∸ suc n = m ∸ n
Rovnost vyjadřuji pomocí následujícího typu. Typ je navržen tak, že term refl typu a ≡ b jde zkonstruovat pouze tehdy, jsou-li a a b stejné:
data _≡_ {A : Set} (x : A) : A → Set where
refl : x ≡ x
Následuje definice závislého páru, kde typ druhé složky závisí na hodnotě první složky:
record Pair (A : Set) (B : A → Set) : Set where
constructor _,_
field
proj₁ : A
proj₂ : B proj₁
Nastavení parseru:
infixl 6 _∸_ infix 4 _≡_ _,_
Funkce vracející typ (tj. výrok), že rozdíl prvních dvou čísel je roven třetímu číslu:
minus_pred : ℕ → ℕ → ℕ → Set minus_pred x y res = x ∸ y ≡ res
Pro tento typ už příkaz Auto vygeneruje požadovanou funkci:
binop₂ : (x : ℕ) → (y : ℕ) → Pair ℕ (minus_pred x y) binop₂ a b = a ∸ b , refl
24.2.2013 22:50
Josef Kufner | skóre: 70
Myslím, že neuniká. V ničem to není lepší. Je to jen příklad, že vlastnost výsledku funkce jde specifikovat typem. V tomto případě to však nemá žádné výhody – spíše naopak.
Příklad praktického použití je třeba funkce, která transformuje program a kde chceme, aby výsledný program dával stejné výsledky jako původní program.
25.2.2013 11:02
Josef Kufner | skóre: 70
Příklad praktického použití je třeba funkce, která transformuje program a kde chceme, aby výsledný program dával stejné výsledky jako původní program.Tohle větou jsi měl celý článek uvést
Vygenerovalo by to neco i kdybych nenadefinoval operator _-_ a minus_pred definoval jinym zpusobem - treba pomoci scitani?
Nejspíš ne.
Konkrétně, pokud máte na mysli podobnou definici
minus_pred : ℕ → ℕ → ℕ → Set minus_pred x y res = y + res ≡ x
tak ne. Problém je v tom, že pro x < y neexistuje přirozené číslo res a Auto hledá totální funkci (všude definovanou).
Kdybych zadefinoval relaci ≥ a funkci binop₂ definoval pouze pro x ≥ y, tak by to stejně nenašel – je to už příliš složité. Nezkoušel jsem to, ale myslím, že by se muselo nadefinovat ∸, pak dokázat lemma, že z x ≥ y a x ∸ y ≡ res plyne y + res ≡ x, a pak by to našel (ale to už není příliš zajímavé, protože je to vlastně celé hotové).
Tiskni
Sdílej:
