Homebrew (Wikipedie), správce balíčků pro macOS a od verze 2.0.0 také pro Linux, byl vydán ve verzi 4.5.0. Na stránce Homebrew Formulae lze procházet seznamem balíčků. K dispozici jsou také různé statistiky.
Byl vydán Mozilla Firefox 138.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 138 je již k dispozici také na Flathubu a Snapcraftu.
Šestnáctý ročník ne-konference jOpenSpace se koná 3. – 5. října 2025 v Hotelu Antoň v Telči. Pro účast je potřeba vyplnit registrační formulář. Ne-konference neznamená, že se organizátorům nechce připravovat program, ale naopak dává prostor všem pozvaným, aby si program sami složili z toho nejzajímavějšího, čím se v poslední době zabývají nebo co je oslovilo. Obsah, který vytvářejí všichni účastníci, se skládá z desetiminutových
… více »Richard Stallman přednáší ve středu 7. května od 16:30 na Technické univerzitě v Liberci o vlivu technologií na svobodu. Přednáška je určená jak odborné tak laické veřejnosti.
Jean-Baptiste Mardelle se v příspěvku na blogu rozepsal o novinkám v nejnovější verzi 25.04.0 editoru videa Kdenlive (Wikipedie). Ke stažení také na Flathubu.
TmuxAI (GitHub) je AI asistent pro práci v terminálu. Vyžaduje účet na OpenRouter.
Byla vydána nová verze R14.1.4 desktopového prostředí Trinity Desktop Environment (TDE, fork KDE 3.5, Wikipedie). Přehled novinek i s náhledy v poznámkách k vydání. Podrobný přehled v Changelogu.
Bylo vydáno OpenBSD 7.7. Opět bez písničky.
V Tiraně proběhl letošní Linux App Summit (LAS) (Mastodon). Zatím nesestříhané videozáznamy přednášek jsou k dispozici na YouTube.
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:
